| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
| |
|
|
| |
This allows for even earlier bootstrapping.
|
| |
|
|
|
|
|
| |
- Remove inclusion of the `tactics` directory, this is coming from a
time loadable modules were found there, now all are under `plugins`.
- Remove 2 dependencies so we can bootstrap coqdep earlier.
- Use `Format` instead of `Printf` for printing.
|
| |
|
|
|
|
|
|
| |
The same warning exists in ocamllibdep so I copied the change there.
Detecting when 2 paths are the same is approximate, eg ././a.ml and
a.ml are considered different. Implementing realpath probably isn't
worth doing for this warning.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
fiat-crypto/OSX
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Note that we don't look inside -arg for eg -coqlib.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
camlp4
|
| | | |
| | |
| | |
| | | |
longer use camlp4.
|
| | |/
|/| |
|
| |\ \ |
|
| | |/ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
|
| |\ \ \
| |/ /
|/| |
| | | |
links (#6697)
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
| |/ |
|
| |\ |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
|
| |/ /
| |
| |
| |
| | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |\ \
| | |
| | |
| | | |
possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
|
| | | | |
|
| | |/
|/| |
|
| | |
| |
| |
| |
| | |
This allows to fix the non-printing of error messages produced when
parsing arguments.
|
| | |
| |
| |
| | |
This was apparently either silently doing nothing or failing.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Nevertheless making option -o of coq_makefile recommended as discussed
in PR#6040.
This is one way to resolve the inconsistency with the usage which says
that all arguments are optional.
|
| |\ \ |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
`make clean`.
|
| | |_|/ / / /
|/| | | | | |
|
| | | |_|_|/
| |/| | |
| | | | |
| | | | | |
Was lost during the coq_makefile 1 -> 2 translation.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Jasper Hugunin
Ralf Jung
Maxime Dénès
Théo Zimmermann
Jim Fehrle
Joachim Breitner
Yannick Forster
Jacques-Pascal Deplaix
Bernhard Schommer
Jason Gross
Enrico Tassi
Hugo Herbelin
Martin Vassor