| Age | Commit message (Collapse) | Author |
|---|
|
|
|
After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.
Test-suite and CI pass after the fix for #8513.
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
|
|
[Dune](https://github.com/ocaml/dune) is a compositional declarative
build system for OCaml. It provides automatic generation of
`version.ml`, `.merlin`, `META`, `opam`, API documentation; install
management; easy integration with external libraries, test runners,
and modular builds.
In particular, Dune uniformly handles components regardless whether
they live in, or out-of-tree. This greatly simplifies cases where a
plugin [or CoqIde] is checked out in the current working copy but then
distributed separately [and vice-versa]. Dune can thus be used as a
more flexible `coq_makefile` replacement.
For now we provide experimental support for a Dune build. In order to
build Coq + the standard library with Dune type:
```
$ make -f Makefile.dune world
```
This PR includes a preliminary, developer-only preview of Dune for
Coq. There is still ongoing work, see
https://github.com/coq/coq/issues/8052 for tracking status towards
full support.
## Technical description.
Dune works out of the box with Coq, once we have fixed some modularity
issues. The main remaining challenge was to support `.vo` files.
As Dune doesn't support custom build rules yet, to properly build
`.vo` files we provide a small helper script `tools/coq_dune.ml`. The
script will scan the Coq library directories and generate the
corresponding rules for `.v -> .vo` and `.ml4 -> .ml` builds. The
script uses `coqdep` as to correctly output the dependencies of
`.v` files. `coq_dune` is akin to `coq_makefile` and should be able to
be used to build Coq projects in the future.
Due to this pitfall, the build process has to proceed in three stages:
1) build `coqdep` and `coq_dune`; 2) generate `dune` files for
`theories` and `plugins`; 3) perform a regular build with all
targets are in scope.
## FAQ
### Why Dune?
Coq has a moderately complex build system and it is not a secret that
many developer-hours have been spent fighting with `make`.
In particular, the current `make`-based system does offer poor support
to verify that the current build rules and variables are coherent, and
requires significant manual, error-prone. Many variables must be
passed by hand, duplicated, etc... Additionally, our make system
offers poor integration with now standard OCaml ecosystem tools such
as `opam`, `ocamlfind` or `odoc`. Another critical point is build
compositionality. Coq is rich in 3rd party contributions, and a big
shortcoming of the current make system is that it cannot be used to
build these projects; requiring us to maintain a custom tool,
`coq_makefile`, with the corresponding cost.
In the past, there has been some efforts to migrate Coq to more
specialized build systems, however these stalled due to a variety of
reasons. Dune, is a declarative, OCaml-specific build tool that is on
the path to become the standard build system for the OCaml ecosystem.
Dune seems to be a good fit for Coq well: it is well-supported, fast,
compositional, and designed for large projects.
### Does Dune replace the make-based build system?
The current, make-based build system is unmodified by this PR and kept
as the default option. However, Dune has the potential
### Is this PR complete? What does it provide?
This PR is ready for developer preview and feedback. The build system
is functional, however, more work is necessary in order to make Dune
the default for Coq.
The main TODOs are tracked at https://github.com/coq/coq/issues/8052
This PR allows developers to use most of the features of Dune today:
- Modular organization of the codebase; each component is built only
against declared dependencies so components are checked for
containment more strictly.
- Hygienic builds; Dune places all artifacts under `_build`.
- Automatic generation of `.install` files, simplified OPAM workflow.
- `utop` support, `-opaque` in developer mode, etc...
- `ml4` files are handled using `coqp5`, a native-code customized
camlp5 executable which brings much faster `ml4 -> ml` processing.
### What dependencies does Dune require?
Dune doesn't depend on any 3rd party package other than the OCaml compiler.
### Some Benchs:
```
$ /usr/bin/time make DUNEOPT="-j 1000" -f Makefile.dune states
59.50user 18.81system 0:29.83elapsed 262%CPU (0avgtext+0avgdata 302996maxresident)k
0inputs+646632outputs (0major+4893811minor)pagefaults 0swaps
$ /usr/bin/time sh -c "./configure -local -native-compiler no && make -j states"
88.21user 23.65system 0:32.96elapsed 339%CPU (0avgtext+0avgdata 304992maxresident)k
0inputs+1051680outputs (0major+5300680minor)pagefaults 0swaps
```
|
|
|
|
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
|
|
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
|
|
|
|
longer use camlp4.
|
|
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
|
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
|
|
|
|
|
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
|
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
When a context variable x is of the form "x := body : Z",
romega is now made aware of this body. Technically, we reify an equation
x = body, and push a corresponding (eq_refl x) as argument of the
final do_omega.
See also the previous commit adding this same feature to omega
(fixing bug 142).
|
|
|
|
|
|
On some benchmarks provided by Chantal Keller a long time ago,
romega was abnormally slow compared to omega (or lia).
It turned out that the change of concl by reified version was
triggering unnecessary unfolds of Z.add, instead of unfolding
ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
the various Parameter Inline : no more indirections, Z_as_Int.plus
is directly Z.add.
Also use Tactics.convert_concl_no_check for this "change", as
recommended by PMP.
|
|
|
|
|
|
|
|
|
|
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.
By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.
Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.
The main changes are:
- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
have different needs with regards to universes/evar_maps, so we
force them to call the (not very safe) `Universes.constr_of_global`
explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
`pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
illustrates the danger of duplication in the code base; the solution
chosen there was to transform the not-found anomaly into an error
message, however the general policy was far from clear. The long
term solution is indeed make `find_reference` emit `Not_found` and
let the client handle the error maybe non-fatally. (so they can test
for constants.
|
|
We remove redundant functions `coq_constant`, `gen_reference`, and
`gen_constant`.
This is a first step towards a lazy binding of libraries references.
We have also chosen to untangle `constr` from `Coqlib`, as how to
instantiate the reference (in particular wrt universes) is a
client-side issue. (The client may want to provide an `evar_map` ?)
c.f. #186
|
|
The trace only mentions the constant k by which we want to divide
the equation, not anymore the equation we obtain after the division.
Shorter trace, and it won't take much more time to perform the few
Z.div than checking as currently the equality of the initial equation
and the final equation multiplied by k.
|
|
|
|
|
|
|
|
We benefit from the fact that we normalize now *all* hypotheses
even the one defining the "stated" variable: it is produced as
...def of v... = v
and normalized as
-v + ...def of v... = 0
which is precisely what we should add to the initial equation during
a O_STATE.
|
|
Now that O_SUM is properly optimized (cf. the [fusion] function),
we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV).
This way, the trace has almost the same size, but ReflOmegaCore.v
is shorter and easier to maintain.
|
|
|
|
|
|
|
|
In this variant, the proof term produced by romega isn't verified at
the tactic run-time (no vm_compute). In theory, [unsafe_romega] should
behave exactly as [romega], but faster. Now, if there's a bug in romega,
we'll be notified only at the following Qed. This could be interesting
for debugging purpose : you could inspect the produced buggish term
via a Show Proof.
|
|
This is a major change :
- Generated proofs are quite shorter, since only the resolution trace remains.
- No time penalty mesured (it even tends to be slightly faster this way).
- Less infrastructure in ReflOmegaCore and refl_omega.
- Warning: the normalization functions in ML and in Coq should be kept
in sync, as well as the variable order.
- Btw: get rid of ML constructor Oufo
|
|
|
|
In a coming commit, we'll normalize terms by a Coq function
that will compare Tvar's instead of blindly applying a trace,
so let's speed-up these comparisons.
|
|
|
|
|
|
|
|
|
|
|
