| Age | Commit message (Collapse) | Author |
|---|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
Ack-by: ppedrot
|
|
and primititive projections
Reviewed-by: maximedenes
|
|
I think the usage looks cleaner this way.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
Reviewed-by: maximedenes
|
|
|
|
(when defining a new constant)
|
|
Reviewed-by: CohenCyril
Fixes a bug introduced by PR #9341
|
|
Grepping for "Error!" is how we decide if we exit with failure or not.
I don't remember why I used the "==> FAILURE <==" string in the
save-logs script but it was an error.
|
|
projections.
This was due to an involuntary capture of a variable name.
|
|
|
|
|
|
|
|
This fixes #9484 .
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Reviewed-by: gares
|
|
Close #5982 #7388 #7483 #9497
|
|
Fixes #9494.
Was failing with "Cannot create self-referring hypothesis" when
the generated name equaled the eqn.
|
|
- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files
cf https://github.com/coq/coq/issues/9464
|
|
This is only used for debugging, if a user wants more feedback she can turn
on the option. Conversely, it has a cost for any tactic script, so it is
wiser to disable it by default.
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
For compatibility, also
* Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs
* Add overlay for HoTT setting Arguments on some instances.
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: fajb
|
|
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
Fixes #9453
|
|
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
Fix #8076.
|
|
It now removes the outdated `CompatOldOldFlag.v` file on `--release`,
and it now correctly updates `bug_9166.v` which seems to specifically be
about the compat flag behavior.
Additionally, it inserts an "autogenerated" notice at top of the two bug
files, and makes them read-only.
|
|
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
This makes the display consistent wrt `TEST`:
```
TEST failure/Case7.v
CHECK Case7
```
vs
```
TEST failure/Case7.v
CHECK failure/Case7.v
```
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
After #8655
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
