| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
longer use camlp4.
|
| |
|
|
|
| |
Since 5ffa147, there is a new clib folder that needed to be added to the set
of includes of ocamldebug
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
| |
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
| | |
|
| |
|
|
|
|
|
| |
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
| | |
|
|
|
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
|
Jim Fehrle
Pierre-Marie Pédrot
Enrico Tassi
Gaëtan Gilbert
Maxime Dénès
Pierre Letouzey