Skip to content

Tactics: make V2 the default #3924

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+26 −25
Open

Tactics: make V2 the default #3924

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e83f8e2
Tactics: make V2 the default
mtzguido Jul 24, 2025
5b17fec
Update tests
mtzguido Oct 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions tests/micro-benchmarks/Misc.Norm3.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ will fail to typecheck. *)
open FStar.Ghost
open FStar.Tactics
open FStar.Reflection.Typing
module R = FStar.Reflection

[@@erasable]
noeq
Expand All @@ -16,21 +17,21 @@ type my_erased (a:Type) = | E of a
let test (r_env goal : _) : Tac unit =
let u0 = pack_universe Uv_Zero in
let goal_typing :
my_erased (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0)))
my_erased (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0)))
= magic()
in
let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0))) =
let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0))) =
match goal_typing with E x -> ()
in
()

(* This should always work regardless of the comment above. *)
let test2 (r_env goal u0 : _) : Tac unit =
let goal_typing :
my_erased (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0)))
my_erased (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0)))
= magic()
in
let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (Tv_Type u0))) =
let goal_typing_tok : squash (typing_token r_env goal (E_Total, pack_ln (R.Tv_Type u0))) =
match goal_typing with E x -> ()
in
()
10 changes: 5 additions & 5 deletions tests/tactics/NoDuplicateSplice.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ module NoDuplicateSplice
open FStar.Tactics

let mk (nm:string) (i:int) : Tac decls =
let lb = pack_lb ({ lb_fv = pack_fv (cur_module() @ [nm])
; lb_us = []
; lb_typ = `int
; lb_def = pack (Tv_Const (C_Int i)) }) in
[pack_sigelt (Sg_Let false [lb])]
let lb = { lb_fv = pack_fv (cur_module() @ [nm])
; lb_us = []
; lb_typ = `int
; lb_def = pack (Tv_Const (C_Int i)) } in
[pack_sigelt (Sg_Let {isrec=false; lbs=[lb]})]

%splice[] (mk "x" 1)

Expand Down
2 changes: 1 addition & 1 deletion ulib/FStar.Reflection.Formula.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@
module FStar.Reflection.Formula

(* This module is a temporary for Meta-F* migration *)
include FStar.Reflection.V1.Formula
include FStar.Reflection.V2.Formula
6 changes: 3 additions & 3 deletions ulib/FStar.Reflection.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,6 @@
*)
module FStar.Reflection

(* This switch currently points to V1. Ask for V2 explicitly by
importing FStar.Reflection.V2 *)
include FStar.Reflection.V1
(* This switch currently points to V2. Ask for V1 explicitly by
importing FStar.Reflection.V1 *)
include FStar.Reflection.V2
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.Builtins.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@
module FStar.Tactics.Builtins

(* This module is a temporary for Meta-F* migration *)
include FStar.Stubs.Tactics.V1.Builtins
include FStar.Stubs.Tactics.V2.Builtins
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.Derived.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@
module FStar.Tactics.Derived

(* This module is a temporary for Meta-F* migration *)
include FStar.Tactics.V1.Derived
include FStar.Tactics.V2.Derived
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.Logic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@
module FStar.Tactics.Logic

(* This module is a temporary for Meta-F* migration *)
include FStar.Tactics.V1.Logic
include FStar.Tactics.V2.Logic
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.SyntaxHelpers.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@
module FStar.Tactics.SyntaxHelpers

(* This module is a temporary for Meta-F* migration *)
include FStar.Tactics.V1.SyntaxHelpers
include FStar.Tactics.V2.SyntaxHelpers
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.V2.Logic.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ open FStar.Reflection.V2.Formula
open FStar.Tactics.NamedView
open FStar.Tactics.Logic.Lemmas {} (* bring lemmas into TC scope *)

(* Repeated to avoid importing FStar.Tactics.V1.Derived. *)
(* Repeated to avoid importing FStar.Tactics.Derived. *)
private let cur_goal () : Tac typ =
let open FStar.Stubs.Tactics.Types in
let open FStar.Stubs.Tactics.V2.Builtins in
Expand Down
2 changes: 1 addition & 1 deletion ulib/FStar.Tactics.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,4 @@
*)
module FStar.Tactics

include FStar.Tactics.V1
include FStar.Tactics.V2
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.Base.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module FStar.InteractiveHelpers.Base

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.Effectful.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module FStar.InteractiveHelpers.Effectful
module HS = FStar.HyperStack

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module FStar.InteractiveHelpers.ExploreTerm

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul
open FStar.InteractiveHelpers.Base

Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.Output.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module FStar.InteractiveHelpers.Output

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module FStar.InteractiveHelpers.PostProcess

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.InteractiveHelpers.Propositions.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module FStar.InteractiveHelpers.Propositions

open FStar.List.Tot
open FStar.Tactics
open FStar.Tactics.V1
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
Expand Down
Loading