Merge branch 'master' into amos/noinlinelet

.completion/fish/fstar.exe.fish

@@ -12,8 +12,7 @@ complete -c fstar.exe -l print_cache_version --description "Print the version fo
 complete -c fstar.exe -l cmi --description "Inline across module interfaces during extraction (aka. cross-module inlining)"
 complete -c fstar.exe -l codegen -r --description "Generate code for further compilation to executable code, or build a compiler plugin"
 complete -c fstar.exe -l codegen-lib --description "namespace  External runtime library (i.e. M.N.x extracts to M.N.X instead of M_N.x)"
-complete -c fstar.exe -l debug --description "module_name  Print lots of debugging information while checking module"
-complete -c fstar.exe -l debug_level -r --description "Control the verbosity of debugging info"
+complete -c fstar.exe -l debug -r --description "Control the verbosity of debugging info"
 complete -c fstar.exe -l defensive -r --description "Enable several internal sanity checks, useful to track bugs and report issues."
 complete -c fstar.exe -l dep -r --description "Output the transitive closure of the full dependency graph in three formats:"
 complete -c fstar.exe -l detail_errors --description "Emit a detailed error report by asking the SMT solver many queries; will take longer"

.docker/base.Dockerfile

@@ -9,7 +9,8 @@
 # will NOT use this file.
 
 # We always try to build against the most current ubuntu image.
-FROM ubuntu:latest
+# FIXME: Broken with 24.04, fixing it to 23.10 so we can keep working
+FROM ubuntu:23.10
 
 RUN apt-get update
 
@@ -22,7 +23,6 @@ RUN apt-get -y --no-install-recommends install vim emacs
 # Base dependencies: opam
 # CI dependencies: jq (to identify F* branch)
 # python3 (for interactive tests)
-# libicu (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
 RUN apt-get install -y --no-install-recommends \
       jq \
       bc \
@@ -34,7 +34,6 @@ RUN apt-get install -y --no-install-recommends \
       sudo \
       python3 \
       python-is-python3 \
-      libicu70 \
       opam \
       && apt-get clean -y
 

Makefile

@@ -57,6 +57,11 @@ bootstrap:
 	+$(Q)$(MAKE) dune-snapshot
 	+$(Q)$(MAKE) fstar
 
+# This is a faster version of bootstrap, since it does not use dune
+# to install the binary and libraries, and instead just copies the binary
+# mannualy. HOWEVER, note that this means plugins will not work well,
+# since they are compiled against the objects in bin/, which will become
+# stale if this rule is used. Using bootstrap is usually safer.
 .PHONY: boot
 boot:
 	+$(Q)$(MAKE) dune-snapshot
@@ -127,10 +132,22 @@ bench:
 # Regenerate and accept expected output tests. Should be manually
 # reviewed before checking in.
 .PHONY: output
-output:
+output: output-error-messages output-ide-emacs output-ide-lsp output-bug-reports
+
+.PHONY: output-error-messages
+output-error-messages:
 	+$(Q)$(MAKE) -C tests/error-messages accept
+
+.PHONY: output-ide-emacs
+output-ide-emacs:
 	+$(Q)$(MAKE) -C tests/ide/emacs accept
+
+.PHONY: output-ide-lsp
+output-ide-lsp:
 	+$(Q)$(MAKE) -C tests/ide/lsp accept
+
+.PHONY: output-bug-reports
+output-bug-reports:
 	+$(Q)$(MAKE) -C tests/bug-reports output-accept
 
 # This rule is meant to mimic what the docker based CI does, but it

examples/dm4free/README.md

@@ -23,7 +23,7 @@ To see more debug output related to the DMFF elaboration and star
 transformations:
 
 ```
-fstar.exe --trace_error --debug_level ED --debug FStar.DM4F.IntST FStar.DM4F.IntST.fst --prn --print_implicits --print_universes --print_bound_var_types
+fstar.exe --trace_error --debug ED FStar.DM4F.IntST.fst --prn --print_implicits --print_universes --print_bound_var_types
 ```
 
 Current status:

examples/dm4free/old/StExn.Handle.fst

@@ -197,7 +197,6 @@ val handle: #a:Type0 -> #wp:wp a -> $f:(unit -> StateExn a wp)
 (*                           match x with  *)
 (*                           | None -> False *)
 (*                           | Some z -> (ens h0 None h1 /\ z=def) \/ ens h0 x h1) *)
-(* #set-options "--debug StExn.Handle --debug_level HACK!"			   *)
 (* let handle2 #a #req #ens f def = *)
 (*   StateExn.reflect (fun h0 -> *)
 (*      match reify (f ()) h0 with *)

examples/dm4free/old/intST.fst

@@ -105,7 +105,7 @@ let put_unfolded (n: int): (n0: int -> PURE (unit * int) (fun post -> post ((),
 let put_cps_type = n:int -> Tot (repr unit (fun n0 post -> post ((), n)))
 let put_cps_type_unfolded = n:int -> Tot (n0: int -> PURE (unit * int) (fun post -> post ((), n)))
 
-(* #reset-options "--debug NatST --debug_level SMTEncoding" *)
+(* #reset-options "--debug SMTEncoding" *)
 
 reifiable reflectable new_effect {
   STATE : a:Type -> wp:wp a -> Effect

examples/dsls/bool_refinement/BoolRefinement.fst

@@ -516,7 +516,7 @@ let weaken (f:RT.fstar_top_env) (sg:src_env) (hyp:var { None? (lookup sg hyp) }
 
 let exp (sg:src_env) = e:src_exp { ln e /\ (forall x. x `Set.mem` freevars e ==> Some? (lookup sg x)) }
 
-#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 6 --query_stats"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 6"
 let rec check (f:RT.fstar_top_env)
               (sg:src_env)
               (e:exp sg)
@@ -650,7 +650,7 @@ let src_refinements_are_closed (e:src_exp {ln e && closed e})
     src_refinements_are_closed_core 0 e elt
 
 
-#push-options "--query_stats --fuel 8 --ifuel 2 --z3rlimit_factor 2"
+#push-options "--fuel 8 --ifuel 2 --z3rlimit_factor 2"
 let rec elab_open_commute' (n:nat) (e:src_exp { ln' e n }) (x:var) 
   : Lemma (ensures
               RT.subst_term (elab_exp e) (RT.open_with_var x n) ==
@@ -949,7 +949,7 @@ let rec as_bindings_rename_env_append (sg sg':src_env) (x y:var)
 let rt_rename (x y:var) : RT.subst_elt =
   RT.NT x (RT.var_as_term y)
 
-#push-options "--query_stats --fuel 8 --ifuel 4 --z3rlimit_factor 10"
+#push-options "--fuel 8 --ifuel 4 --z3rlimit_factor 10"
 let rec rename_elab_commute_core (m:int) (e:src_exp { ln' e m } ) (x y:var) (n:nat)
   : Lemma 
     (ensures RT.subst_term (elab_exp e) (RT.shift_subst_n n [rt_rename x y]) ==
@@ -1123,7 +1123,7 @@ let sub_typing_renaming (#f:RT.fstar_top_env)
     | S_ELab g _ _ d ->
       S_ELab _ _ _ (core_subtyping_renaming sg sg' x y b t0 t1 d)
 
-#push-options "--query_stats --fuel 2 --ifuel 2 --z3rlimit_factor 2"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2"
 let freevars_included_in (e:src_exp) (sg:src_env) =
   forall x. x `Set.mem` freevars e ==> Some? (lookup sg x)
 
@@ -1685,12 +1685,15 @@ let soundness_lemma (f:RT.fstar_top_env)
       (fun dd -> FStar.Squash.return_squash (soundness dd))
 
 let main (nm:string) (src:src_exp) : RT.dsl_tac_t =
-  fun f ->
+  fun (f, expected_t) ->
   if ln src && closed src
-  then 
-    let (| src_ty, _ |) = check f [] src in
-    soundness_lemma f [] src src_ty;
-    [RT.mk_checked_let f nm (elab_exp src) (elab_ty src_ty)]
+  then if None? expected_t
+       then let (| src_ty, _ |) = check f [] src in
+            soundness_lemma f [] src src_ty;
+            [],
+            RT.mk_checked_let f (T.cur_module ()) nm (elab_exp src) (elab_ty src_ty),
+            []
+       else T.fail "Bool refinement DSL: no support for expected type yet"
   else T.fail "Not locally nameless"
 
 (***** Examples *****)

examples/dsls/dependent_bool_refinement/DependentBoolRefinement.fst

@@ -105,7 +105,7 @@ let open_ty t v = open_ty' t (EVar v) 0
 let close_ty t v = close_ty' t v 0
 let open_ty_with t e = open_ty' t e 0
 
-#push-options "--query_stats --fuel 4 --ifuel 2 --z3rlimit_factor 8"
+#push-options "--fuel 4 --ifuel 2 --z3rlimit_factor 8"
 let rec open_exp_freevars (e:src_exp) (v:src_exp) (n:nat)
   : Lemma 
     (ensures (freevars e `Set.subset` freevars (open_exp' e v n))  /\
@@ -472,7 +472,7 @@ and check_ok (e:src_exp) (sg:src_env)
     | EApp e1 e2 -> check_ok e1 sg && check_ok e2 sg
 
 
-#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 6 --query_stats"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 6"
 
 let rec check (f:fstar_top_env)
               (sg:src_env)
@@ -578,7 +578,7 @@ let rec extend_env_l_lookup_bvar (g:R.env) (sg:src_env) (x:var)
     | [] -> ()
     | hd :: tl -> extend_env_l_lookup_bvar g tl x
 
-#push-options "--query_stats --fuel 8 --ifuel 2 --z3rlimit_factor 2"
+#push-options "--fuel 8 --ifuel 2 --z3rlimit_factor 2"
 let rec elab_open_commute' (n:nat) (e:src_exp) (x:src_exp) 
   : Lemma (ensures
               RT.subst_term (elab_exp e) [ RT.DT n (elab_exp x) ] ==
@@ -638,15 +638,15 @@ let rec extend_env_l_lookup_fvar (g:R.env) (sg:src_env) (fv:R.fv)
     | [] -> ()
     | hd::tl -> extend_env_l_lookup_fvar g tl fv
 
-#push-options "--query_stats --fuel 2 --ifuel 2 --z3rlimit_factor 2"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2"
 
 let subtyping_soundness #f (#sg:src_env) (#t0 #t1:src_ty) (ds:sub_typing f sg t0 t1)
   : GTot (RT.sub_typing (extend_env_l f sg) (elab_ty t0) (elab_ty t1))
   = match ds with
     | S_Refl _ _ -> RT.Rel_equiv _ _ _ _ (RT.Rel_refl _ _ _)
     | S_ELab _ _ _ d -> d
 
-#push-options "--query_stats --fuel 8 --ifuel 2 --z3rlimit_factor 4"
+#push-options "--fuel 8 --ifuel 2 --z3rlimit_factor 4"
 let rec elab_close_commute' (n:nat) (e:src_exp) (x:var)
   : Lemma (ensures
               RT.subst_term (elab_exp e) [ RT.ND x n ] ==
@@ -878,10 +878,13 @@ and closed_ty (t:src_ty)
 
 let main (nm:string) (src:src_exp)
   : RT.dsl_tac_t
-  = fun f -> 
+  = fun (f, expected_t) -> 
       if closed src
-      then 
-        let (| src_ty, _ |) = check f [] src in
-        soundness_lemma f [] src src_ty;
-        [RT.mk_checked_let f nm (elab_exp src) (elab_ty src_ty)]
+      then if None? expected_t
+           then let (| src_ty, _ |) = check f [] src in
+                soundness_lemma f [] src src_ty;
+                [],
+                RT.mk_checked_let f (T.cur_module ()) nm (elab_exp src) (elab_ty src_ty),
+                []
+           else T.fail "Dependent bool refinement DSL: no support for expected type yet"
       else T.fail "Not locally nameless"

examples/dsls/stlc/STLC.Core.fst

@@ -1,3 +1,19 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
 module STLC.Core
 module T = FStar.Tactics.V2
 module R = FStar.Reflection.V2
@@ -537,12 +553,15 @@ let soundness_lemma (sg:stlc_env)
       (fun dd -> FStar.Squash.return_squash (soundness dd g))
 
 let main (nm:string) (src:stlc_exp) : RT.dsl_tac_t =
-  fun g ->
+  fun (g, expected_t) ->
   if ln src && closed src
-  then
-    let (| src_ty, d |) = check g [] src in
-    soundness_lemma [] src src_ty g;
-    [RT.mk_checked_let g nm (elab_exp src) (elab_ty src_ty)]
+  then if None? expected_t
+       then let (| src_ty, d |) = check g [] src in
+            soundness_lemma [] src src_ty g;
+            [],
+            RT.mk_checked_let g (T.cur_module ()) nm (elab_exp src) (elab_ty src_ty),
+            []
+       else T.fail "STLC Core DSL: no support for expected type yet"
   else T.fail "Not locally nameless"
 
 (***** Tests *****)

examples/dsls/stlc/STLC.Infer.fst

@@ -1,3 +1,19 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
 module STLC.Infer
 module T = FStar.Tactics.V2
 module R = FStar.Reflection.V2
@@ -123,10 +139,10 @@ let rec elab_core g (e:stlc_exp R.term)
 
 let main (nm:string) (e:stlc_exp unit)
   : RT.dsl_tac_t
-  = fun g -> 
+  = fun (g, expected_t) ->
       let (| e, _ |) = infer g [] e in
       let e = elab_core g e in
-      Core.main nm e g
+      Core.main nm e (g, expected_t)
 
 (***** Tests *****)
 

examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.fst

@@ -14,7 +14,7 @@ open Negotiation
 module U32 = FStar.UInt32
 module B = LowStar.Buffer
 
-#push-options "--z3rlimit 16 --query_stats"
+#push-options "--z3rlimit 16"
 
 inline_for_extraction
 noextract

examples/miniparse/MiniParse.fst.config.json

@@ -0,0 +1,7 @@
+{
+  "fstar_exe": "fstar.exe",
+  "options": [
+  ],
+  "include_dirs": [
+  ]
+}

examples/native_tactics/Imp.Fun.Driver.fst

@@ -47,6 +47,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.Fun.Driver --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

examples/native_tactics/Imp.Fun.DriverNBE.fst

@@ -48,6 +48,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.Fun.DriverNBE --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

examples/native_tactics/Imp.Fun.fst

@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Imp.Fun
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.Fun
 
@@ -167,7 +167,7 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Registers.Imp --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
 // let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

examples/native_tactics/Imp.List.Driver.fst

@@ -47,6 +47,6 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.List.Driver --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

examples/native_tactics/Imp.List.DriverNBE.fst

@@ -48,5 +48,5 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Imp.List.DriverNBE --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))

examples/native_tactics/Imp.List.fst

@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Imp.List
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.List
 

examples/native_tactics/Makefile

@@ -54,7 +54,7 @@ all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))
 	touch $@
 
 %.sep.test: %.fst %.ml
-	$(FSTAR) $*.Test.fst --load $* --debug $* --debug_level tactics
+	$(FSTAR) $*.Test.fst --load $*
 	touch $@
 
 %.ml: %.fst

examples/native_tactics/Registers.Imp.fst

@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Registers.Imp
-//#set-options "--debug Imp --debug_level SMTQuery"
+//#set-options "--debug SMTQuery"
 open FStar.Mul
 module R = Registers.List
 
@@ -167,7 +167,7 @@ let normal #a (e:a) =
 
 let norm_assert (p:Type) : Lemma (requires (normal p)) (ensures True) = ()
 
-#set-options "--debug Registers.Imp --debug_level print_normalized_terms --admit_smt_queries true"
+#set-options "--debug print_normalized_terms --admit_smt_queries true"
 // let _ = norm_assert (forall (x:int) rm. R.sel (eval' (Seq [Const x (reg 0)]) rm) 0 == x) // eval' (Seq [Const x (reg 0)]) rm == rm)
 let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))
 // let _ = norm_assert (forall x y. equiv_norm (long_zero x) (long_zero y))