Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
remove all mentions of "fstarlib, fstartaclib, fstar-tactics-lib"
  • Loading branch information
tahina-pro committed Feb 1, 2023
1 parent f9f2d4e commit 35e5a7c
Show file tree
Hide file tree
Showing 26 changed files with 31 additions and 141 deletions.
1 change: 0 additions & 1 deletion .completion/fish/fstar.exe.fish
Expand Up @@ -49,7 +49,6 @@ complete -c fstar.exe -l max_ifuel --description "non-negative integer Number o
complete -c fstar.exe -l MLish --description "Trigger various specializations for compiling the F* compiler itself (not meant for user code)"
complete -c fstar.exe -l no_default_includes --description "Ignore the default module search paths"
complete -c fstar.exe -l no_extract --description "module name Deprecated: use --extract instead; Do not extract code from this module"
complete -c fstar.exe -l no_load_fstartaclib --description "Do not attempt to load fstartaclib by default"
complete -c fstar.exe -l no_location_info --description "Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)"
complete -c fstar.exe -l no_smt --description "Do not send any queries to the SMT solver, and fail on them instead"
complete -c fstar.exe -l normalize_pure_terms_for_extraction --description "Extract top-level pure terms after normalizing them. This can lead to very large code, but can result in more partial evaluation and compile-time specialization."
Expand Down
8 changes: 4 additions & 4 deletions .scripts/process_build.sh
Expand Up @@ -86,13 +86,13 @@ else
echo -e "* ${GREEN}PASSED!${NC} for examples/hello"
fi

diag "-- Rebuilding ulib/ml (to make sure it works) --"
make -C ulib rebuild
diag "-- Rebuilding ulib (to make sure it works) --"
make -j6 dune-bootstrap
if [ $? -ne 0 ]; then
echo -e "* ${RED}FAIL!${NC} for install-fstarlib - make returned $?"
echo -e "* ${RED}FAIL!${NC} for dune-bootstrap - make returned $?"
exit 1
else
echo -e "* ${GREEN}PASSED!${NC} for install-fstarlib"
echo -e "* ${GREEN}PASSED!${NC} for dune-bootstrap"
fi

diag "-- Verify all examples --"
Expand Down
5 changes: 2 additions & 3 deletions INSTALL.md
Expand Up @@ -336,9 +336,8 @@ This does three things:
special `flexlink` technology for this. See `examples/crypto` and
`contrib/CoreCrypto/ml` for examples.

2. It builds the various OCaml libraries (`fstar-compiler-lib`, `fstarlib`,
`fstartaclib`), needed for building OCaml code extracted from F\*, native
tactics, etc.
2. It builds the various OCaml libraries needed for building OCaml
code extracted from F\*, native tactics, etc.

3. It verifies the F\* standard library, producing `.checked` files that cache
definitions to speed up subsequent usage.
Expand Down
2 changes: 2 additions & 0 deletions bin/run_benchmark.sh
Expand Up @@ -20,6 +20,8 @@ set -o pipefail
# informative stats. This script automates the process of running with
# orun and summarizing the results.

# FIXME: recast those benchmarks

help () {
cat <<EOF
$0: Benchmark F*
Expand Down
6 changes: 3 additions & 3 deletions doc/book/part1/part1_execution.rst
Expand Up @@ -125,7 +125,7 @@ native code library (a cmxa file) with ``ocamlbuild``, as shown below

.. code-block::
OCAMLPATH=$FSTAR_HOME/bin ocamlbuild -use-ocamlfind -pkg batteries -pkg fstarlib Part1_Quicksort_Generic.cmxa
OCAMLPATH=$FSTAR_HOME/bin ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib Part1_Quicksort_Generic.cmxa
Some points to note:

Expand All @@ -136,7 +136,7 @@ Some points to note:
* The ``-use-ocamlfind`` option enables a utility to find OCaml libraries.

* Extracted F* programs rely on two libraries: ``batteries`` and
``fstarlib``, which is what the ``-pkg`` options say.
``fstar.lib``, which is what the ``-pkg`` options say.

* Finally, ``Part1_Quicksort_Generic.cmxa`` references the name of
the corresponding ``.ml`` file, but with the ``.cmxa`` extension
Expand Down Expand Up @@ -200,7 +200,7 @@ You can compile this code in OCaml to a native executable by doing:

.. code-block::
OCAMLPATH=$FSTAR_HOME/bin ocamlbuild -use-ocamlfind -pkg batteries -pkg fstarlib Part1_Quicksort_Main.native
OCAMLPATH=$FSTAR_HOME/bin ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib Part1_Quicksort_Main.native
And, finally, you can execute Part1_Quicksort_Main.native to see the
following output:
Expand Down
3 changes: 0 additions & 3 deletions examples/crypto/Makefile
Expand Up @@ -89,9 +89,6 @@ CONTRIB_LIBS=$(FSTAR_UCONTRIB)/CoreCrypto/ml/CoreCrypto.cmxa

include $(FSTAR_ULIB)/ml/Makefile.include

#OCAMLOPT automatically contains fstarlib
SUPPORT_LIBS=$(FSTARLIB_DIR)/fstarlib.cmxa

$(CONTRIB_LIBS):
+$(MAKE) -C $(FSTAR_UCONTRIB)

Expand Down
2 changes: 1 addition & 1 deletion examples/hello/multifile/Makefile
Expand Up @@ -16,7 +16,7 @@ endif
#cache_dir: where to find checked files
#odir: where to put all output artifacts
#include: where to find source and checked files
#already_cached: fstarlib is already built
#already_cached: fstar ulib is already built

FSTAR=$(FSTAR_EXE) \
--cache_dir $(OUTPUT_DIR) \
Expand Down
1 change: 0 additions & 1 deletion examples/native_tactics/Makefile
@@ -1,6 +1,5 @@
FSTAR_HOME=../..
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs

# Tests for which the native tactics used in module named Sample.Test.fst are
# declared in a corresponding module named Sample.fst
Expand Down
1 change: 0 additions & 1 deletion examples/native_tactics/Makefile.bench
@@ -1,6 +1,5 @@
FSTAR_HOME=../..
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs

.SECONDARY:
.PRECIOUS:
Expand Down
23 changes: 12 additions & 11 deletions examples/tactics/Makefile
Expand Up @@ -37,14 +37,15 @@ else
stringprintertest:
endif

FStar.Tactics.CanonCommSemiring.cmxs FStar.Tactics.CanonCommMonoid.cmxs:
$(FSTAR) --cache_checked_modules --codegen Plugin --extract 'FStar.Tactics.CanonCommSemiring FStar.Tactics.CanonCommMonoid FStar.Tactics.CanonCommSwaps' FStar.Tactics.CanonCommSemiring.fst
rm -f ./*.cmxs
cat FStar.Tactics.CanonCommMonoid.ml.fixup >> FStar.Tactics.CanonCommMonoid.ml
cat FStar.Tactics.CanonCommSemiring.ml.fixup >> FStar.Tactics.CanonCommSemiring.ml
env OCAMLPATH="../../bin/" ocamlfind ocamlopt -shared -I . -package fstar-tactics-lib -o ./FStar.Tactics.CanonCommMonoid.cmxs ./FStar.Tactics.CanonCommSwaps.ml ./FStar.Tactics.CanonCommMonoid.ml
env OCAMLPATH="../../bin/" ocamlfind ocamlopt -shared -I . -package fstar-tactics-lib -o ./FStar.Tactics.CanonCommSemiring.cmxs ./FStar.Tactics.CanonCommSwaps.ml ./FStar.Tactics.CanonCommMonoid.ml ./FStar.Tactics.CanonCommSemiring.ml

canon-native: FStar.Tactics.CanonCommSemiring.cmxs FStar.Tactics.CanonCommMonoid.cmxs
$(FSTAR) --load FStar.Tactics.CanonCommMonoid FStar.Tactics.CanonCommMonoid.fst
$(FSTAR) --load FStar.Tactics.CanonCommSemiring FStar.Tactics.CanonCommSemiring.fst
# FIXME: is this still needed?
# FStar.Tactics.CanonCommSemiring.cmxs FStar.Tactics.CanonCommMonoid.cmxs:
# $(FSTAR) --cache_checked_modules --codegen Plugin --extract 'FStar.Tactics.CanonCommSemiring FStar.Tactics.CanonCommMonoid FStar.Tactics.CanonCommSwaps' FStar.Tactics.CanonCommSemiring.fst
# rm -f ./*.cmxs
# cat FStar.Tactics.CanonCommMonoid.ml.fixup >> FStar.Tactics.CanonCommMonoid.ml
# cat FStar.Tactics.CanonCommSemiring.ml.fixup >> FStar.Tactics.CanonCommSemiring.ml
# env OCAMLPATH="../../bin/" ocamlfind ocamlopt -shared -I . -package fstar-tactics-lib -o ./FStar.Tactics.CanonCommMonoid.cmxs ./FStar.Tactics.CanonCommSwaps.ml ./FStar.Tactics.CanonCommMonoid.ml
# env OCAMLPATH="../../bin/" ocamlfind ocamlopt -shared -I . -package fstar-tactics-lib -o ./FStar.Tactics.CanonCommSemiring.cmxs ./FStar.Tactics.CanonCommSwaps.ml ./FStar.Tactics.CanonCommMonoid.ml ./FStar.Tactics.CanonCommSemiring.ml

# canon-native: FStar.Tactics.CanonCommSemiring.cmxs FStar.Tactics.CanonCommMonoid.cmxs
# $(FSTAR) --load FStar.Tactics.CanonCommMonoid FStar.Tactics.CanonCommMonoid.fst
# $(FSTAR) --load FStar.Tactics.CanonCommSemiring FStar.Tactics.CanonCommSemiring.fst
1 change: 0 additions & 1 deletion examples/tactics/Makefile.Bane
Expand Up @@ -14,7 +14,6 @@ include .depend
%.fsti.checked:
$(FSTAR) $<

FSTARTACLIB=$(FSTAR_HOME)/bin/fstar-tactics-lib/fstartaclib.cmxs
CACHE = _cache

%.cmxs: %.Lib.fst.checked
Expand Down
23 changes: 1 addition & 22 deletions ocaml/fstar-lib/FStar_Tactics_Load.ml
Expand Up @@ -7,18 +7,6 @@ module O = FStar_Options
let perr s = if O.debug_any () then U.print_error s
let perr1 s x = if O.debug_any () then U.print1_error s x

let find_taclib_old () =
let default = FStar_Options.fstar_bin_directory ^ "/fstar-tactics-lib" in
try
begin
let r = Process.run "ocamlfind" [| "query"; "fstar-tactics-lib" |] in
match r with
| { Process.Output.exit_status = Process.Exit.Exit 0; stdout; _ } ->
String.trim (List.hd stdout)
| _ -> default
end
with _ -> default

let dynlink fname =
try
perr ("Attempting to load " ^ fname ^ "\n");
Expand All @@ -35,18 +23,9 @@ type load_ops_t = {

let load_ops : load_ops_t =
let already_loaded = ref None in
let load_old () =
dynlink (find_taclib_old () ^ "/fstartaclib.cmxs");
perr "Loaded old fstartaclib successfully\n";
"fstar-tactics-lib"
in
let load_lib () =
if !already_loaded = None then
let taclib =
try
load_old ()
with _ -> "fstar.lib" (* assume that we are in the new setting where the F* compiler is linked with fstar.lib *)
in
let taclib = "fstar.lib" in
already_loaded := Some taclib
in
{
Expand Down
1 change: 0 additions & 1 deletion src/.gitignore
Expand Up @@ -4,7 +4,6 @@ fsharp-output
/backend/
u_boot_fsts
u_ocaml-output
.fstarlib

dep.graph

Expand Down
8 changes: 0 additions & 8 deletions src/basic/FStar.Options.fst
Expand Up @@ -195,7 +195,6 @@ let defaults =
("MLish" , Bool false);
("no_default_includes" , Bool false);
("no_extract" , List []);
("no_load_fstartaclib" , Bool false);
("no_location_info" , Bool false);
("no_smt" , Bool false);
("no_plugins" , Bool false);
Expand Down Expand Up @@ -381,7 +380,6 @@ let get_max_ifuel () = lookup_opt "max_ifuel"
let get_MLish () = lookup_opt "MLish" as_bool
let get_no_default_includes () = lookup_opt "no_default_includes" as_bool
let get_no_extract () = lookup_opt "no_extract" (as_list as_string)
let get_no_load_fstartaclib () = lookup_opt "no_load_fstartaclib" as_bool
let get_no_location_info () = lookup_opt "no_location_info" as_bool
let get_no_plugins () = lookup_opt "no_plugins" as_bool
let get_no_smt () = lookup_opt "no_smt" as_bool
Expand Down Expand Up @@ -947,11 +945,6 @@ let rec specs_with_types warn_unsafe : list (char * string * opt_type * string)
Accumulated (PathStr "module name"),
"Deprecated: use --extract instead; Do not extract code from this module");
( noshort,
"no_load_fstartaclib",
Const (Bool true),
"Do not attempt to load fstartaclib by default");
( noshort,
"no_location_info",
Const (Bool true),
Expand Down Expand Up @@ -1777,7 +1770,6 @@ let no_default_includes () = get_no_default_includes ()
let no_extract s = get_no_extract() |> List.existsb (module_name_eq s)
let normalize_pure_terms_for_extraction
() = get_normalize_pure_terms_for_extraction ()
let no_load_fstartaclib () = get_no_load_fstartaclib ()
let no_location_info () = get_no_location_info ()
let no_plugins () = get_no_plugins ()
let no_smt () = get_no_smt ()
Expand Down
1 change: 0 additions & 1 deletion src/basic/FStar.Options.fsti
Expand Up @@ -159,7 +159,6 @@ val ml_ish : unit -> bool
val set_ml_ish : unit -> unit
val no_default_includes : unit -> bool
val no_extract : string -> bool
val no_load_fstartaclib : unit -> bool
val no_location_info : unit -> bool
val no_plugins : unit -> bool
val no_smt : unit -> bool
Expand Down
2 changes: 0 additions & 2 deletions src/fstar/FStar.Main.fst
Expand Up @@ -91,8 +91,6 @@ let load_native_tactics () =
let cmxs_files = (modules_to_load@cmxs_to_load) |> List.map cmxs_file in
if Options.debug_any () then
Util.print1 "Will try to load cmxs files: %s\n" (String.concat ", " cmxs_files);
if not (Options.no_load_fstartaclib ()) then
Tactics.Load.try_load_lib ();
Tactics.Load.load_tactics cmxs_files;
iter_opt (Options.use_native_tactics ()) Tactics.Load.load_tactics_dir;
()
Expand Down
10 changes: 2 additions & 8 deletions src/ocaml-output/Makefile
Expand Up @@ -154,22 +154,16 @@ $(FStar_Version_ml):
# installs we cannot assume the user has git installed.)
install_dir = cd ../../$(1) && find . -type f -exec $(INSTALL_EXEC) -m 644 -D {} $(PREFIX)/$(2)/{} \;
# install the standard library binary files
install_fstarlib = $(INSTALL_EXEC) -m 755 -D ../../$(1)/$(2) $(PREFIX)/lib/fstar/$(2)
# Install FStar into $(PREFIX) using the standard Unix directory
# structure. NOTE: this rule needs ocamlfind to install the fstarlib,
# fstar-tactics-lib and fstar-compiler-lib packages. It works with the
# structure. NOTE: this rule works with the
# opam package, but it has not been tested in any other settings.
install:
@# Install the binary
$(INSTALL_EXEC) -m 755 -D $(FSTAR_MAIN_NATIVE) $(PREFIX)/bin/fstar.exe
@# Then the standard library
$(call install_dir,ulib,lib/fstar)
@# Then the binary library
cd ../../bin/fstarlib && ocamlfind install fstarlib *
cd ../../bin/fstar-compiler-lib && ocamlfind install fstar-compiler-lib *
cd ../../bin/fstar-tactics-lib && ocamlfind install fstar-tactics-lib *
true # FIXME: install the contents of the local lib/fstar
@# Then the rest of the static files.
@# (those are not used in the opam package, not sure if their Makefiles work)
$(call install_dir,examples,share/fstar/examples)
Expand Down
2 changes: 1 addition & 1 deletion src/parser/FStar.Parser.Dep.fst
Expand Up @@ -1714,7 +1714,7 @@ let print_full (deps:deps) : unit =
in
//And, if this is not an interface, we also print out the dependences among the .ml files
// excluding files in ulib, since these are packaged in fstarlib.cmxa
// excluding files in ulib, since these are packaged in fstar_lib.cmxa
let all_fst_files_dep, widened =
if Options.cmi()
then profile
Expand Down
2 changes: 1 addition & 1 deletion src/reflection/FStar.Reflection.Data.fsti
Expand Up @@ -155,6 +155,6 @@ type exp =
| Var of var
| Mult of exp * exp

(* Needed so this appears in the ocaml output for fstar-tactics-lib *)
(* Needed so this appears in the ocaml output for the fstar tactics library *)
type decls = list sigelt

2 changes: 1 addition & 1 deletion tests/bug-reports/Bug460.fst
Expand Up @@ -39,7 +39,7 @@ let main = print_test ()

(*
$ bin/fstar.exe examples/bug-reports/bug460.fst --codegen OCaml
$ ocamlfind ocamlopt -package batteries,stdint,fileutils,sqlite3,zarith -linkpkg -g -thread -w a+A-27 -I ulib/ml/ ulib/ml/fstarlib.cmxa Bug460.ml -o Bug460
$ ocamlfind ocamlopt -package batteries,stdint,fileutils,sqlite3,zarith,fstar.lib -linkpkg -g -thread -w a+A-27 Bug460.ml -o Bug460
$ ./Bug460
Test (x = y) = true
Test (x = z) = false
Expand Down
6 changes: 0 additions & 6 deletions ulib/.gitignore
@@ -1,12 +1,6 @@
*.fst-ver
*.fsti-ver
*.mgen
ml/extracted
ml/fstarlib.mllib
tactics_ml/extracted
tactics_ml/fstarlib_leftovers
tactics_ml/fstartaclib.mllib
.depend.extract
.depend.extract.fsharp
.depend.extract.rsp
.depend.extract-stdlib
Expand Down
2 changes: 0 additions & 2 deletions ulib/FStar.Tactics.Typeclasses.fst
Expand Up @@ -15,8 +15,6 @@
*)
module FStar.Tactics.Typeclasses

(* TODO: This must be in the FStar.Tactics.* namespace or we fail to build
* fstarlib. That seems silly, but I forget the details of the library split. *)
open FStar.List.Tot
open FStar.Tactics
module T = FStar.Tactics
Expand Down
1 change: 0 additions & 1 deletion ulib/Makefile
Expand Up @@ -36,7 +36,6 @@ clean: clean_checked clean_ocaml
$(Q)rm -f .depend.extract.rsp
$(Q)rm -f .depend.extract
$(Q)rm -f *.checked.lax .cache/*.checked.lax
$(Q)rm -fr ml/extracted tactics_ml/extracted tactics_ml/fstarlib_leftovers

clean_ocaml:
@echo "[CLEAN OCAML LIBS]"
Expand Down
53 changes: 0 additions & 53 deletions ulib/fstarlib_leftovers.ml

This file was deleted.

2 changes: 1 addition & 1 deletion ulib/ml/Makefile.include
Expand Up @@ -9,7 +9,7 @@ else
endif
FSTARLIB=$(FSTARLIB_DIR)/fstar_lib.cmxa

# Left as an example if we were to add multiple versions of fstarlib
# Left as an example if we were to add multiple versions of fstar ulib
# ifeq ($(MEM),HST)
# OCAML_DEFAULT_FLAGS=-predicates hyperstack
# endif
Expand Down
4 changes: 0 additions & 4 deletions ulib/ml/fstar-compiler-lib-META

This file was deleted.

0 comments on commit 35e5a7c

Please sign in to comment.