FStarLang · mtzguido · Aug 11, 2025 · Aug 11, 2025
diff --git a/lib/steel/Steel.Channel.Simplex.fst b/lib/steel/Steel.Channel.Simplex.fst
@@ -349,7 +349,6 @@ let recv_availableT (#p:sprot) #q (cc:chan q) (vs vr:chan_val) (_:unit)
     Steel.SpinLock.release cc.chan_lock;
     vs_msg
 
-#push-options "--ide_id_info_off"
 let send_receive_prelude (#p:prot) (cc:chan p)
   : SteelT (chan_val & chan_val)
            emp

diff --git a/lib/steel/Steel.DisposableInvariant.fst b/lib/steel/Steel.DisposableInvariant.fst
@@ -23,8 +23,6 @@ open Steel.Effect
 open Steel.FractionalPermission
 open Steel.Reference
 
-#push-options "--ide_id_info_off"
-
 [@@__reduce__]
 let conditional_inv (r:ghost_ref bool) (p:vprop) =
       (fun (b:bool) ->

diff --git a/lib/steel/Steel.DisposableInvariant.fsti b/lib/steel/Steel.DisposableInvariant.fsti
@@ -26,8 +26,6 @@ open Steel.FractionalPermission
 /// while allowing to reclaim the locked resource once the lock is not needed anymore.
 /// This is analogous to Cancellable Invariants in Iris.
 
-#push-options "--ide_id_info_off"
-
 /// The abstract type of ghost locks. Only used for proof purposes, will be erased at extraction time
 val inv (p:vprop) : Type0
 

diff --git a/lib/steel/Steel.Effect.Atomic.fsti b/lib/steel/Steel.Effect.Atomic.fsti
@@ -22,7 +22,7 @@ include Steel.Effect.Common
 
 /// This module defines atomic and ghost variants of the Steel effect
 
-#set-options "--warn_error -330 --ide_id_info_off"  //turn off the experimental feature warning
+#set-options "--warn_error -330"  //turn off the experimental feature warning
 
 
 (*** SteelAGCommon effect ***)

diff --git a/lib/steel/Steel.Effect.Common.fsti b/lib/steel/Steel.Effect.Common.fsti
@@ -24,7 +24,6 @@ open FStar.Ghost
 /// different Steel effects.
 /// It also contains the tactic responsible for frame inference through a variant of AC-unification
 
-#set-options "--ide_id_info_off"
 
 (* Normalization helpers *)
 

diff --git a/lib/steel/Steel.Effect.fst b/lib/steel/Steel.Effect.fst
@@ -21,7 +21,6 @@ module Mem = Steel.Memory
 open Steel.Semantics.Instantiate
 module FExt = FStar.FunctionalExtensionality
 
-#set-options "--ide_id_info_off"
 
 let _:squash (forall p q. can_be_split p q == Mem.slimp (hp_of p) (hp_of q)) = reveal_can_be_split ()
 

diff --git a/lib/steel/Steel.Effect.fsti b/lib/steel/Steel.Effect.fsti
@@ -26,7 +26,6 @@ include Steel.Effect.Common
 /// selectors, which will be discharged by SMT
 
 #set-options "--warn_error -330"  //turn off the experimental feature warning
-#set-options "--ide_id_info_off"
 
 (* Defining the Steel effect with selectors *)
 

diff --git a/lib/steel/Steel.GhostMonotonicHigherReference.fst b/lib/steel/Steel.GhostMonotonicHigherReference.fst
@@ -31,7 +31,6 @@ module PR = Steel.GhostPCMReference
 module A = Steel.Effect.Atomic
 open FStar.Real
 
-#set-options "--ide_id_info_off"
 
 let ref a p = PR.ref (history a p) pcm_history
 

diff --git a/lib/steel/Steel.GhostPCMReference.fsti b/lib/steel/Steel.GhostPCMReference.fsti
@@ -27,7 +27,6 @@ open Steel.Effect
 /// This module exposes the core PCM-based memory model defined in Steel.Memory
 /// as ghost Steel computations.
 
-#set-options "--ide_id_info_off"
 
 /// The type of a reference to ghost state in pcm [p]
 [@@erasable]

diff --git a/lib/steel/Steel.HigherReference.fst b/lib/steel/Steel.HigherReference.fst
@@ -24,7 +24,6 @@ open Steel.PCMFrac
 open FStar.Real
 module RP = Steel.PCMReference
 
-#set-options "--ide_id_info_off"
 
 module Mem = Steel.Memory
 

diff --git a/lib/steel/Steel.MonotonicHigherReference.fst b/lib/steel/Steel.MonotonicHigherReference.fst
@@ -30,7 +30,6 @@ module M = Steel.Memory
 module PR = Steel.PCMReference
 open FStar.Real
 
-#set-options "--ide_id_info_off"
 
 let ref a p = M.ref (history a p) pcm_history
 

diff --git a/lib/steel/Steel.PCMReference.fsti b/lib/steel/Steel.PCMReference.fsti
@@ -26,7 +26,6 @@ open Steel.Effect
 /// This module exposes the core PCM-based memory model defined in Steel.Memory
 /// as stateful Steel computations.
 
-#set-options "--ide_id_info_off"
 
 /// Lifting the pts_to separation logic, PCM-indexed predicate to a vprop.
 /// Its selector is non-informative (it is unit)

diff --git a/lib/steel/Steel.Primitive.ForkJoin.Unix.fst b/lib/steel/Steel.Primitive.ForkJoin.Unix.fst
@@ -28,7 +28,6 @@ open Steel.Reference
 open Steel.Primitive.ForkJoin
 
 #set-options "--warn_error -330"  //turn off the experimental feature warning
-#set-options "--ide_id_info_off"
 
 // (* Some helpers *)
 let change_slprop_equiv (p q : vprop)

diff --git a/lib/steel/Steel.Reference.fst b/lib/steel/Steel.Reference.fst
@@ -24,7 +24,6 @@ module Mem = Steel.Memory
 module H = Steel.HigherReference
 module U = FStar.Universe
 
-#set-options "--ide_id_info_off"
 
 let ref a = H.ref (U.raise_t a)
 

diff --git a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst
@@ -23,7 +23,7 @@ open Steel.Effect.Atomic
 
 /// This module defines atomic and ghost variants of the Steel effect
 
-#set-options "--warn_error -330 --ide_id_info_off"  //turn off the experimental feature warning
+#set-options "--warn_error -330"  //turn off the experimental feature warning
 
 let repr (a:Type u#a)
          (already_framed:bool)

diff --git a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti
@@ -41,7 +41,7 @@ module STF = Steel.ST.Effect
 /// [pure_post] abbreviations. The tactic in Steel.Effect.Common relies
 /// on those names to distinguish between vprop and non-vprop goals.
 
-#set-options "--warn_error -330 --ide_id_info_off"  //turn off the experimental feature warning
+#set-options "--warn_error -330"  //turn off the experimental feature warning
 
 (*** STAGCommon effect ***)
 val repr (a:Type u#a)               //result type

diff --git a/lib/steel/Steel.ST.Effect.fst b/lib/steel/Steel.ST.Effect.fst
@@ -21,7 +21,6 @@ open FStar.Ghost
 include Steel.Effect.Common
 open Steel.Effect
 #set-options "--warn_error -330"  //turn off the experimental feature warning
-#set-options "--ide_id_info_off"
 
 let repr a framed pre post req ens : Type u#2 =
   Steel.Effect.repr a framed pre post (fun _ -> req) (fun _ v _ -> ens v)

diff --git a/lib/steel/Steel.ST.Effect.fsti b/lib/steel/Steel.ST.Effect.fsti
@@ -24,7 +24,6 @@ open Steel.Memory
 open FStar.Ghost
 include Steel.Effect.Common
 #set-options "--warn_error -330"  //turn off the experimental feature warning
-#set-options "--ide_id_info_off"
 
 val repr (a:Type)
          (framed:bool)

diff --git a/lib/steel/Steel.ST.PCMReference.fsti b/lib/steel/Steel.ST.PCMReference.fsti
@@ -24,7 +24,6 @@ open Steel.ST.Util
 /// This module exposes the core PCM-based memory model defined in Steel.Memory
 /// as stateful Steel computations.
 
-#set-options "--ide_id_info_off"
 
 /// Lifting the pts_to separation logic, PCM-indexed predicate to a vprop.
 /// Its selector is non-informative (it is unit)

diff --git a/lib/steel/Steel.ST.Printf.fst b/lib/steel/Steel.ST.Printf.fst
@@ -59,7 +59,6 @@ module L = FStar.List.Tot
 module A = Steel.ST.Array
 module U32 = FStar.UInt32
 
-#set-options "--ide_id_info_off"
 
 /// `lmbuffer a l` is
 ///    - an array of `a`

diff --git a/lib/steel/Steel.ST.Util.fst b/lib/steel/Steel.ST.Util.fst
@@ -21,7 +21,6 @@ module SEA = Steel.Effect.Atomic
 module SE = Steel.Effect
 open Steel.ST.Coercions
 
-#set-options "--ide_id_info_off"
 
 let weaken #o p q l =
   coerce_ghost (fun () -> SEA.rewrite_slprop p q l)

diff --git a/lib/steel/Steel.SpinLock.fst b/lib/steel/Steel.SpinLock.fst
@@ -22,7 +22,7 @@ open Steel.Effect
 open Steel.Reference
 open Steel.FractionalPermission
 
-#set-options "--ide_id_info_off --fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 let available = false
 let locked = true

diff --git a/share/steel/examples/steel/CQueue.LList.fst b/share/steel/examples/steel/CQueue.LList.fst
@@ -17,8 +17,6 @@ let cllist_head #a c =
 let cllist_tail #a c =
   c.tail
 
-#push-options "--ide_id_info_off"
-
 let cllist0_refine
   (#a: Type0)
   (c: cllist_ptrvalue a)

diff --git a/share/steel/examples/steel/CQueue.fst b/share/steel/examples/steel/CQueue.fst
@@ -1,7 +1,6 @@
 module CQueue
 open CQueue.LList
 
-#set-options "--ide_id_info_off"
 
 //Re-define squash, since this module explicitly
 //replies on proving equalities of the form `t_of v == squash p`

diff --git a/share/steel/examples/steel/DList.Invariant.fst b/share/steel/examples/steel/DList.Invariant.fst
@@ -569,8 +569,6 @@ let intro_dlist_snoc_cons #a #u (left tail head:t a) (hd: cell a) (xs:_)
         dlist_snoc left tail head (next hd) (hd :: xs))
   = sladmit()
 
-#push-options "--ide_id_info_off"
-
 let new_dlist' (#a:Type) (init:a)
   : Steel (t a & cell a)
     emp

diff --git a/share/steel/examples/steel/DList.fst b/share/steel/examples/steel/DList.fst
@@ -8,8 +8,6 @@ open Steel.Reference
 open DList.Invariant
 module U = Steel.Utils
 
-#push-options "--ide_id_info_off"
-
 let new_dlist (#a:Type) (init:a)
   : Steel (t a & cell a)
     emp

diff --git a/share/steel/examples/steel/DList1.fst b/share/steel/examples/steel/DList1.fst
@@ -594,7 +594,6 @@ let intro_dlist_snoc_cons #a #u (left tail head:t a) (hd: erased (cell a)) (xs:e
         dlist_snoc left tail head (next hd) (econs hd xs))
   = rewrite_slprop _ _ (fun m -> dlist_snoc_cons left tail head hd xs)
 
-#push-options "--ide_id_info_off"
 let enil #a (x:erased a) : erased (list a) = hide [reveal x]
 
 let new_dlist' (#a:Type) (init:a)

diff --git a/share/steel/examples/steel/LList.ST.fst b/share/steel/examples/steel/LList.ST.fst
@@ -24,7 +24,6 @@ open Steel.ST.Util
 
 open Steel.ST.Reference
 
-#set-options "--ide_id_info_off"
 
 let rec is_list #a ll l : Tot vprop (decreases l) =
   match l with

diff --git a/share/steel/examples/steel/LList.fst b/share/steel/examples/steel/LList.fst
@@ -7,7 +7,6 @@ open Steel.Reference
 include LList.Invariant
 module L = FStar.List.Tot.Base
 
-#set-options "--ide_id_info_off"
 
 let rec datas (#a:Type) (l:list (cell a)) : list a =
   match l with

diff --git a/share/steel/examples/steel/LList32.fst b/share/steel/examples/steel/LList32.fst
@@ -27,7 +27,6 @@ module G = FStar.Ghost
 
 /// Monomorphization of LList.ST for UInt32
 
-#set-options "--ide_id_info_off"
 
 type u32 = FStar.UInt32.t
 

diff --git a/share/steel/examples/steel/OWGCounter.ST.fst b/share/steel/examples/steel/OWGCounter.ST.fst
@@ -46,7 +46,6 @@ module GR = Steel.ST.GhostReference
  *   protected by a lock
  *)
 
-#set-options "--ide_id_info_off"
 
 let half_perm = half_perm full_perm
 

diff --git a/share/steel/examples/steel/OWGCounter.fst b/share/steel/examples/steel/OWGCounter.fst
@@ -42,7 +42,7 @@ open Steel.Effect
 module R = Steel.Reference
 module P = Steel.FractionalPermission
 
-#set-options "--ide_id_info_off --using_facts_from '* -FStar.Tactics -FStar.Reflection' --fuel 0 --ifuel 0"
+#set-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --fuel 0 --ifuel 0"
 
 let half_perm = half_perm full_perm
 

diff --git a/share/steel/examples/steel/OWGCounterInv.fst b/share/steel/examples/steel/OWGCounterInv.fst
@@ -41,7 +41,7 @@ module P = Steel.FractionalPermission
 
 open Steel.DisposableInvariant
 
-#set-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --fuel 0 --ifuel 0 --ide_id_info_off"
+#set-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --fuel 0 --ifuel 0"
 
 (**** A few wrappers over library functions ****)
 

diff --git a/share/steel/examples/steel/Queue.fst b/share/steel/examples/steel/Queue.fst
@@ -3,7 +3,6 @@ module Queue
 module L = FStar.List.Tot
 open Steel.Utils {} // patterns
 
-#set-options "--ide_id_info_off"
 
 let pure_upd_next
   (#a: Type0)
@@ -197,8 +196,6 @@ let new_queue #a v =
   intro_exists ([v]) (queue_l pc pc);
   return pc
 
-#push-options "--ide_id_info_off --print_implicits"
-
 let witness_h_exists_erased (#a:Type) (#opened_invariants:_) (#p: Ghost.erased a -> vprop) (_:unit)
   : SteelGhostT (Ghost.erased a) opened_invariants
                 (h_exists p) (fun x -> p x)

diff --git a/share/steel/examples/steel/SelectorLogic.fst b/share/steel/examples/steel/SelectorLogic.fst
@@ -5,8 +5,6 @@ module Mem = Steel.Memory
 
 (* Extending selectors to support wand; establishing a correspondence with linear logic *)
 
-#push-options "--ide_id_info_off"
-
 let selector (hp:slprop) (a:(hmem hp) -> Type) = (h:hmem hp -> GTot (a h))
 
 /// The basis of our selector framework: Separation logic assertions enhanced with selectors

diff --git a/share/steel/examples/steel/Selectors.Examples.fst b/share/steel/examples/steel/Selectors.Examples.fst
@@ -6,7 +6,7 @@ open Steel.Reference
 
 /// A few small tests for the selector effect.
 
-#push-options "--fuel 0 --ifuel 0 --ide_id_info_off"
+#push-options "--fuel 0 --ifuel 0"
 
 let swap (#a:Type0) (r1 r2:ref a) : Steel unit
   (vptr r1 `star` vptr r2)

diff --git a/share/steel/examples/steel/Selectors.Tree.Core.fsti b/share/steel/examples/steel/Selectors.Tree.Core.fsti
@@ -6,7 +6,6 @@ open Steel.Reference
 
 module Spec = Trees
 
-#set-options "--ide_id_info_off"
 
 (*** Type declarations *)
 

diff --git a/share/steel/examples/steel/Selectors.Tree.fst b/share/steel/examples/steel/Selectors.Tree.fst
@@ -9,7 +9,7 @@ open Steel.Reference
 /// The implementation of the Selectors.Tree interface.
 /// Predicates prefixed by (**) correspond to stateful lemmas for folding and unfolding the tree predicate
 
-#set-options "--fuel 1 --ifuel 1 --z3rlimit 50 --ide_id_info_off"
+#set-options "--fuel 1 --ifuel 1 --z3rlimit 50"
 
 let rec append_left #a ptr v =
   if is_null_t ptr then (

diff --git a/share/steel/examples/steel/Selectors.Tree.fsti b/share/steel/examples/steel/Selectors.Tree.fsti
@@ -7,7 +7,6 @@ open Steel.Effect
 
 module Spec = Trees
 
-#set-options "--ide_id_info_off"
 
 /// This module provides a library of operations on trees.
 /// The definition of the `linked_tree` predicate is hidden behind the `Selectors.Tree.Core` interface.

diff --git a/share/steel/examples/steel/TwoLockQueue.fst b/share/steel/examples/steel/TwoLockQueue.fst
@@ -16,8 +16,6 @@ module Q = Queue
 /// ensuring that at most one enqueue (resp. dequeue) is happening at any time
 /// We only prove that this implementation is memory safe, and do not prove the functional correctness of the concurrent queue
 
-#push-options "--ide_id_info_off"
-
 /// Adding the definition of the vprop equivalence to the context, for proof purposes
 let _: squash (forall p q. p `equiv` q <==> hp_of p `Steel.Memory.equiv` hp_of q) =
   Classical.forall_intro_2 reveal_equiv

diff --git a/share/steel/tests/SteelIntroExists.fst b/share/steel/tests/SteelIntroExists.fst
@@ -124,7 +124,6 @@ open Steel.Effect.Common
 open Steel.ST.GenElim
 
 
-#set-options "--ide_id_info_off"
 
 assume val test_2626_aux
   (#opened: _)

diff --git a/share/steel/tutorial/ExtractRefs.fst b/share/steel/tutorial/ExtractRefs.fst
@@ -9,7 +9,7 @@ module U32 = FStar.UInt32
 
 /// Some examples using Steel references with fractional permissions
 
-#push-options "--fuel 0 --ifuel 0 --ide_id_info_off"
+#push-options "--fuel 0 --ifuel 0"
 
 (** Swap examples **)
 

diff --git a/share/steel/tutorial/References.fst b/share/steel/tutorial/References.fst
@@ -8,7 +8,7 @@ open Steel.Reference
 
 /// Some examples using Steel references with fractional permissions
 
-#push-options "--fuel 0 --ifuel 0 --ide_id_info_off"
+#push-options "--fuel 0 --ifuel 0"
 
 (** Swap examples **)
 

diff --git a/src/proofs/steelc/Steel.ST.C.Types.Base.fst b/src/proofs/steelc/Steel.ST.C.Types.Base.fst
@@ -346,8 +346,6 @@ let hr_share_imbalance (#a:Type)
 = HR.share #_ #_ #_ #v r;
   _
 
-#set-options "--ide_id_info_off"
-
 let pts_to_equiv
   r1 r2 v
 = rewrite (ref_equiv r1 r2) (ref_equiv0 r1 r2);
Original file line number	Diff line number	Diff line change
Expand Up		@@ -27,7 +27,6 @@ module G = FStar.Ghost

		/// Monomorphization of LList.ST for UInt32

		#set-options "--ide_id_info_off"

		type u32 = FStar.UInt32.t

Expand Down
-Original file line number
+Diff line change
@@ Expand Up / @@ -46,7 +46,6 @@ module GR = Steel.ST.GhostReference @@
      *   protected by a lock
      *)
-    #set-options "--ide_id_info_off"
     let half_perm = half_perm full_perm
@@ Expand Down @@
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,7 +6,6 @@ open Steel.Reference

		module Spec = Trees

		#set-options "--ide_id_info_off"

		(*** Type declarations *)

Expand Down