| Age | Commit message (Collapse) | Author |
|---|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.
|
|
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
This is the smallest possible change to clarify the text without making it
even more formal.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
Fixes #10909: Set Default Proof Mode is not documented.
|
|
|
|
The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification. This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.
|
|
Close #11036
|
|
Reviewed-by: jfehrle
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
|
|
This increases backwards compatibility. If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
|
|
Also add a tactic notation so that it takes in uconstrs by default.
Also add some basic tests for `rapply`.
Also document rapply in the manual
|
|
Close #9634
|
|
Ack-by: Zimmi48
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
Only the deprecated one was documentated, and the deprecation was not
mentioned.
|
|
|
|
relation
Reviewed-by: gares
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
|
|
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
|
|
document « Property »
more documentation fixes
[doc] destructed → destructured
[doc] another le_minus→lt_1_r
[doc] @jfehrle suggestions
[doc] more minor fixes
|
|
This is the dual of #10344.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82
|
|
reduce or not.
Reviewed-by: jfehrle
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
