| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
|
|
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v
- test-suite/failure/inductive4.v is now .../inductive.v
- repro for #4157 now added to the repo (it was in an unmerged commit
on @herbelin's repo)
- commit message of 244d7a9aa contains a repro for its bug (I didn't
bother adding to the test suite as a return of the bug could just as
well use different strings so the specific repro wouldn't test
anything useful)
|
|
|
|
It now uses the origin/master branch rather than the master branch, thus
avoiding the need for local merges.
More importantly, it no longer creates a subshell in case of conflicts,
but instead gives control back to the user. Once conflicts are solved, it
suffices to relaunch the script (instead of exiting the subshell). The
reason is that, otherwise, there was no sane way of giving up a backport,
due to the infinite subshell loop.
|
|
|
|
proj
Ack-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
to an archive subfolder.
Reviewed-by: ejgallego
|
|
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
tested, only binary GTK)
|
|
- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile
|
|
|
|
|
|
|
|
|
|
|
|
The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767).
|
|
|
|
subfolder.
|
|
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.
Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.
As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.
This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
|
|
This is routine as for API doc writers to be able to access the newer
features.
|
|
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
As requested by Gaëtan Gilbert, we add shims
- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`
that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.
`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states && bin/coqtop` under the old model.
This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.
In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]
We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.
The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.
This will work for `dir=stdlib/Init/` for example, or for any other
combination.
|
|
PG would do it by default but since we override coq-prog-args it
doesn't.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: vbgl
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
|
|
|
|
|
|
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
|
|
Supersedes #8718.
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
