Skip to content

Commit

Permalink
Revert "Introduce --ocamlenv"
Browse files Browse the repository at this point in the history
This reverts commit 601584597385bed967e161f58be3884b23d2c65e.
  • Loading branch information
mtzguido committed Oct 14, 2024
1 parent 440ccc9 commit f03938a
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 40 deletions.
7 changes: 0 additions & 7 deletions src/basic/FStarC.Options.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1631,13 +1631,6 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
"locate_ocaml",
Const (Bool true),
text "Print the root of the built OCaml F* library and exit");
( noshort,
"ocamlenv",
WithSideEffect ((fun _ -> print_error "--ocamlenv must be the first argument, see fstar.exe --help for details\n"; exit 1),
(Const (Bool true))),
text "With no arguments: print an environment suitable for a shell (similar to 'opam env'). \
With arguments: run a command in that environment. \
NOTE: this must be the FIRST argument passed to F* and other options are NOT processed.");
]
and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) =
Expand Down
37 changes: 4 additions & 33 deletions src/fstar/FStarC.Main.fst
Original file line number Diff line number Diff line change
Expand Up @@ -113,28 +113,10 @@ let load_native_tactics () =
(* print_in_place options are passed *)
let fstar_files: ref (option (list string)) = Util.mk_ref None

(* ocamlenv mode: called whenever the *first* argument is exactly 'ocamlenv' *)
let go_ocamlenv rest_args =
let shellescape s = s in
let ocamldir = Find.locate_ocaml () in
let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in
let new_ocamlpath = ocamldir ^ ":" ^ old_ocamlpath in
match rest_args with
| [] ->
Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" (shellescape new_ocamlpath);
exit 0
| cmd :: args ->

Util.putenv "OCAMLPATH" new_ocamlpath;
Util.execvp cmd (cmd :: args)
| _ ->
let open FStarC.Pprint in
Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [
Errors.Msg.text "Unrecognized usage of --ocamlenv";
]

(* Normal mode with some flags, files, etc *)
let go_normal () =
(****************************************************************************)
(* Main function *)
(****************************************************************************)
let go _ =
let res, filenames = process_args () in
if Options.trace_error () then begin
let h = get_sigint_handler () in
Expand Down Expand Up @@ -303,17 +285,6 @@ let go_normal () =
Errors.raise_error0 Errors.Error_MissingFileName "No file provided"
end

(****************************************************************************)
(* Main function *)
(****************************************************************************)

(* choose a main driver function and go *)
let go () =
let args = Util.get_cmd_args () in
match args with
| _ :: "--ocamlenv" :: rest -> go_ocamlenv rest
| _ -> go_normal ()

(* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *)
let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax.Syntax.term
= match k with
Expand Down

0 comments on commit f03938a

Please sign in to comment.