| Age | Commit message (Collapse) | Author |
|---|
|
This is the first release that contains the type-safe grammar API.
|
|
The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).
We also add a `-bytecode-compiler` flag.
Fixes #4607
|
|
|
|
Fixes #8621
|
|
|
|
|
|
These are unused and not likely to come back.
|
|
Fix silly typo that created havoc in developer out-of-the-box setups.
|
|
In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.
However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.
While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
|
|
Dune calls `./configure` under the build sandbox, which, if the voboot
target has not been executed will contain only the OCaml parts of Coq.
Thus, we make configure not to die if the `plugins` directory is not
present.
This makes Dune usable without calling the `voboot` target.
|
|
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
|
|
After #8043 was fixed we can come back to a stricter warning profile
for flambda.
|
|
This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.
We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
|
|
|
|
|
|
Fixes #8067. This is becoming the default in many developments, so it
makes sense to require it too, both for Coq and for Plugins.
|
|
We turn all Coq warnings that are on by default into errors.
|
|
See https://github.com/ocaml/num/issues/9
|
|
flambda happy.
See issue #8043.
Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like
an OCaml bug.
|
|
They are not used anymore.
People should use Proof-General (and optionally Company-Coq) instead.
|
|
|
|
|
|
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.
|
|
|
|
|
|
Bumping to 4.02.3 was decided some time ago in the WG, however a
couple of places escaped updating.
|
|
|
|
|
|
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.
|
|
Currently, `configure.ml` does copy/link some files from `kernel` to
`checker` in an ad-hoc way. Instead, it is preferable to add a copy
rule to make and let it handle the dependencies properly.
This also fixes a dependency bug in Windows, as files wouldn't be
properly refreshed if `configure` was not run each time.
|
|
|
|
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
|
|
Warnings are just too hard to see. Also there is no point keeping a
noop option except to point people at the replacement, which does not
require configure to succeed.
|
|
|
|
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|
|
|
|
|
|
Some messages were sometimes not printed because of the missing flushes.
We use a generic combinator suggested by Emilio.
|
|
|
|
|
|
In this way it is easy to support multiple defaults
|
|
|
|
longer use camlp4.
|
|
The hook created checks to see if dev/tools/pre-commit exists, and, if
so, runs it. This way, we don't have to do any fancy logic to update
the git pre-commit hook. The configure script never overwrites an
existing precommit hook, so users can disable it by creating an empty
pre-commit hook.
The check for existence is so that if users check out an old version of
Coq, attempting to commit won't give an error about non-existent files.
|
|
|
|
|
|
2.18.3
|
|
|
|
The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0
even for much newer versions. This makes building Coq on Ubuntu
impossible without modifying configure. This commit fixes that problem.
See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for
the upstream bug.
This closes #6585
|
|
|
