| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We turn all Coq warnings that are on by default into errors.
|
|
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|
Coqpp has nothing to do with `grammar`, we thus place it in its own
directory, which will prove convenient in more modular build systems.
Note that we add `coqpp` to the list of global includes, we could have
indeed added some extra rules, but IMHO not worth it as hopefully
proper containment will be soon checked by Dune.
|
|
|
|
|
|
coqtop.opt$(EXE).
|
|
points of Camlp5
|
|
steps.
|
|
Fixes #7758.
|
|
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
|
Fixes #7666. Due to shared mapping of executables Linux doesn't allow
to overwrite binaries that are running; we do as `ocamlopt` and delete
the target file before copy.
|
|
|
|
|
|
Caused by a semantic conflict with the separate toplevels PR.
|
|
The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.
Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q
Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.
This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp
|
|
|
|
|
|
It seems that it is standard practice in the OCaml world to set the
`-cclib` flags at library creation time, at least in native libraries.
Indeed, this seems to make linking easier as seen for example in #7563.
|
|
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 makes it easier to compile our executables for debug purposes.
|
|
Instead of playing static linking games, we just ship two different
top-level files depending on whether we want to enable `Drop` support
[bytecode case] or not.
The savings of the old approach [1 line of code] were not worth the
complexities of the linking hack.
|
|
|
|
camlp4
|
|
longer use camlp4.
|
|
We correctly set the path of `libcoqrun` in non-local builds. This bug
was introduced by #6038.
c.f. #6475 , #5992.
|
|
|
|
|
|
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
|
|
|
|
|
|
|
|
|
Enable builds on Windows by removing Windows-style endings where it impacts make.
The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
|
|
|
|
|
|
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.
|
|
When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.
This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.
Fixes #6364.
|
|
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.
|
|
This allows us to enforce that it works without breaking the build
when it doesn't.
|
|
Mismatch probably caused by c5aca4005.
|
|
structure.
|
|
The test was abandoned at the time of merging subdirectory browsing
between coqdep and coqtop, and to limit at the same time the
dependency of coqdep in files such as unicode.cmo.
But checking ident validity speeds up browsing in arbitrary directory
structure and we restore it for this reason.
(One could also say that browsing arbitrary directory structures is
not intended, but in practice this may happen, as e.g. reported in
BZ#5734.)
|
|
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|
Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72.
There seem to have been no actual errors due to this, only ocaml
complaining about missing .cmi files.
|
|
to escape non-UTF-8 file names)
|
