diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-28 21:02:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-10 18:41:16 +0100 |
| commit | 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f (patch) | |
| tree | 7bf3135dea14dfccac59a6b373549b6bddec7741 /lib | |
| parent | d0f89f8c59cda2e7e74fec693e511e910fbc0434 (diff) | |
[build] Remove coqmktop in favor of ocamlfind.
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 12 | ||||
| -rw-r--r-- | lib/flags.ml | 8 | ||||
| -rw-r--r-- | lib/flags.mli | 6 |
3 files changed, 5 insertions, 21 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 206d75033..8ebf84057 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -153,19 +153,17 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind +let ocamlfind () = Coq_config.ocamlfind (** {2 Camlp4 paths} *) let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) let camlp4bin () = - if !Flags.camlp4bin_spec then !Flags.camlp4bin else - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () - with Not_found -> - Coq_config.camlp4bin + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () + with Not_found -> + Coq_config.camlp4bin let camlp4 () = camlp4bin () / exe Coq_config.camlp4 diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..97795faa6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -179,14 +179,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..e4710a126 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,12 +143,6 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int |