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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/build/windows/ReadMe.txt | 2 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index a6d8e4462..7e80e33c6 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -418,7 +418,6 @@ Binary file ./bin/coqchk.exe matches Binary file ./bin/coqdep.exe matches Binary file ./bin/coqdoc.exe matches Binary file ./bin/coqide.exe matches -Binary file ./bin/coqmktop.exe matches Binary file ./bin/coqtop.byte.exe matches Binary file ./bin/coqtop.exe matches Binary file ./bin/coqworkmgr.exe matches @@ -438,7 +437,6 @@ Binary file ./bin/ocamldoc.exe matches Binary file ./bin/ocamldoc.opt.exe matches Binary file ./bin/ocamlfind.exe matches Binary file ./bin/ocamlmklib.exe matches -Binary file ./bin/ocamlmktop.exe matches Binary file ./bin/ocamlobjinfo.exe matches Binary file ./bin/ocamlopt.exe matches Binary file ./bin/ocamlopt.opt.exe matches diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0c6d3ee80..26f3d0ddc 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ |