Merge pull request #3336 from mtzguido/splice_no_lax

Tactics: make splice_t always run without admit/lax
FStarLang · Jun 29, 2024 · 2f0f45f · 2f0f45f
2 parents 6af102c + fb70958
commit 2f0f45f
Show file tree

Hide file tree

Showing 7 changed files with 67 additions and 14 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml
diff --git a/src/tactics/FStar.Tactics.Hooks.fst b/src/tactics/FStar.Tactics.Hooks.fst
@@ -891,7 +891,7 @@ let splice
             : list goal & dsl_tac_result_t =
             run_tactic_on_ps tau.pos tau.pos false
               FStar.Tactics.Typeclasses.solve
-              ({env with gamma=[]}, val_t)
+              ({env with lax=false; admit=false; gamma=[]}, val_t)
               FStar.Tactics.Typeclasses.solve
               tau
               tactic_already_typed

diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst
@@ -572,6 +572,9 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
 
   (* If we're --laxing, and this is not an `expect_lax_failure`, then just ignore the definition *)
   | Sig_fail {fail_in_lax=false} when not (Env.should_verify env) || Options.admit_smt_queries () ->
+    if Debug.any () then
+      BU.print1 "Skipping %s since env.admit=true and this is not an expect_lax_failure\n"
+        (Print.sigelt_to_string_short se);
     [], [], env
 
   | Sig_fail {errs=expected_errors; fail_in_lax=lax; ses} ->

diff --git a/tests/error-messages/OptionStack.fst b/tests/error-messages/OptionStack.fst
@@ -15,14 +15,25 @@
 *)
 module OptionStack
 
+assume val p : int -> prop
+
+[@@expect_failure]
+let t0 = assert (p 1)
+
+[@@expect_failure]
+let t1 = assert (p 2)
+
 [@@expect_failure]
-let _ = assert False
+let t2 = assert False
 
 #push-options "--admit_smt_queries true"
 
-let _ = assert False
+let t3 = assert False
+let t4 = assert False
+let t5 = assert False
+let t6 = assert False
 
 #pop-options
 
 [@@expect_failure]
-let _ = assert False
+let t7 = assert False
diff --git a/tests/error-messages/OptionStack.fst.expected b/tests/error-messages/OptionStack.fst.expected
@@ -1,17 +1,33 @@
 >> Got issues: [
-* Error 19 at OptionStack.fst(19,8-19,14):
+* Error 19 at OptionStack.fst(21,9-21,15):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also OptionStack.fst(19,15-19,20)
+  - See also OptionStack.fst(21,16-21,21)
 
 >>]
 >> Got issues: [
-* Error 19 at OptionStack.fst(28,8-28,14):
+* Error 19 at OptionStack.fst(24,9-24,15):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also OptionStack.fst(28,15-28,20)
+  - See also OptionStack.fst(24,16-24,21)
+
+>>]
+>> Got issues: [
+* Error 19 at OptionStack.fst(27,9-27,15):
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also OptionStack.fst(27,16-27,21)
+
+>>]
+>> Got issues: [
+* Error 19 at OptionStack.fst(39,9-39,15):
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also OptionStack.fst(39,16-39,21)
 
 >>]
 Verified module: OptionStack

diff --git a/tests/tactics/Admit.fst b/tests/tactics/Admit.fst
@@ -0,0 +1,16 @@
+module Admit
+
+open FStar.Tactics.V2
+
+#push-options "--admit_smt_queries true"
+let test () : squash False =
+  _ by (
+    ()
+  )
+#pop-options
+
+[@@expect_failure [19]]
+let test2 () : squash False =
+  _ by (
+    ()
+  )