| Age | Commit message (Collapse) | Author |
|---|
|
to an archive subfolder.
Reviewed-by: ejgallego
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
subfolder.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
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.
|
|
Reviewed-by: cpitclaudel
|
|
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.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: vbgl
|
|
|
|
|
|
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.
|
|
Fixes #9537
This way, users can do:
```
dune exec coqtop.byte
> Drop.
# #directory "dev";;
# #use "include_dune";;
```
|
|
Related: coq/bignums#17
[ci skip]
|
|
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.
|
|
Apparently it's deprecated / doesn't always work, see
https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m
See #9429 (we also need to fix the distributed file on the server).
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
In response to review comments by Zimmi48
|
|
We now support --master and --release. On the master branch, we support
four compatibility versions, while on releases and release branches, we
support only three compatibility versions.
We also support --git-add to automatically run `git add` with new and
updated files, and to run `git rm` with deleted files.
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
|
|
|
|
|
|
|
We do a couple of changes:
- Splitting notation keys into more categories to make table smaller.
This should (a priori) make printing faster (see #6416).
- Abbreviations are treated for printing like single notations: they
are pushed to the scope stack, so that in a situation such as
Open Scope foo_scope.
Notation foo := term.
Open Scope bar_scope.
one looks for notations first in scope bar_scope, then try to use
foo, they try for notations in scope foo_scope.
- We seize the opportunity of this commit to simplify
availability_of_notation which is now integrated to
uninterp_notation and which does not have to be called explicitly
anymore.
|
|
|
|
|
|
|
|
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
Now that the checker is using the regular kernel files it can also use
the normal printers.
|
|
Following discussion in #7042, we write down an advice to give time
for last comments before merging potentially controversial PRs.
We document a practice that is becoming standard in order to improve
PR merging time: some other maintainer can self-assign if the main
maintainer is not responding.
Encourage component maintainers to announce when they won't be available.
We document the practice of code owner teams.
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
|
|
|
|
We update the docs for the removal of `Sigma` and the deprecation of
`enter_nf`.
|
|
As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):
```
dune exec dev/dune-dbg
(ocd) source dune_db
```
or
```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```
for the checker.
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
|
|
|
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
|
|
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This satisfies a wish by @ppedrot
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
|
