| Age | Commit message (Collapse) | Author |
|---|
|
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)
This commit moves stm specific arguments parsing to stm/stmargs.ml
|
|
|
|
This fixes a regression introduced in #11618, where I didn't realize
that the order of ML includes would be important as users may want to
shadow it.
In general I do believe that shadowing is tricky and the build system
should handle it, but for now makes sense to preserver the behavior.
The fix is not very nice, but we cannot afford to tweak the API as
this should be backported to 8.12.1; there is a pending PR refactoring
a bit more the toplevel init that should clean this up.
Fixes #12771
|
|
Add headers to a few files which were missing them.
|
|
We refactor handling of `-boot` so the "coqlib" guessing routine,
`Envars.coqlib ()` is not called when bootstrapping.
In compositional builds involving Coq's prelude we don't want for this
guessing to happen, as the heuristics to locate the prelude will fail
due to different build layout choices.
Thus after this patch Coq does not do any guessing when `-boot` is
passed, leaving the location of libraries to the usual command line
parameters.
Note that some other tooling still calls `Envars.coqlib`, however this
should happen late enough as for it to be safe; we will fix that
eventually when we consolidate the library for library handling among
tools.
Ideally, we would also remove `Envars.coqlib` altogether, as we want
to avoid clients accessing the Coq filesystem in a non-controlled way.
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
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.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
This is useful when we want to have finer control of the location of
files in the bootstrap process, for example when building using Dune.
Also, this makes options consistent with what `coqdep` already uses
for bootstrap.
The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust.
Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
|
|
`theories` now never have `.ml` files inside.
|
|
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
|
|
As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .
In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.
Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.
We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.
Closes #6446
Example with backtrace from https://github.com/coq/coq/issues/11366
Old:
```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
New:
```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
|
|
We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]
This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.
Logic could be pushed upwards, but this is good enough for now.
This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.
The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .
|
|
Absolute paths follow different separator rules so "c:\foo/bar" may
not work on `mingw`.
We try to improve this situation using OCaml's `Filename.dir_sep/concat`
|
|
When initilazing the load path, coqtop adds implicit bindings for stdlib
and for the current directory (-R stdlib Coq -R . ""). In case of
a clash, the binding of the current directory had priority, which makes
it impossible to edit stdlib files (when they Require files from the
same directory) using PG, or from CoqIDE when launched from the directory
containing the file.
Example to reproduce the problem:
```
cd plugins/omega
coqide Omega.v
```
some of the Requires will fail.
|
|
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
|
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
|
|
|
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
|
|
|
|
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
|
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
|
|
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
|
We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.
To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:
```
type add_ml = AddNoML | AddTopML | AddRecML
type vo_path_spec = {
unix_path : string; (* Filesystem path contaning vo/ml files *)
coq_path : Names.DirPath.t; (* Coq prefix for the path *)
implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
}
type coq_path_spec =
| VoPath of vo_path_spec
| MlPath of string
type coq_path = {
path_spec: coq_path_spec;
recursive: bool;
}
```
Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.
This API is necessarily internal [for now] thus I don't think a
changes entry is needed.
|
|
One less global flag.
|
|
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
|
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
|
|
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
|
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
|
We remove `init_library_roots` as there is no point in resetting this
internal variable. Its only user is `init_load_path` and this function
is not meant (and is not) idempotent now.
|
|
`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.
This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.
|
|
|
|
|
|
|
|
|
|
|
|
versions.
|
|
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
|
and avoid duplication
|
|
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
|
|
|
|
Was PR#290: Add a compatibility flag for 8.6 and refactor.
|
|
|
|
|
|
It seems that such options were adding the considered path to the ML loadpath
as well, which is not what is documented, and does not provide an atomic way
to manipulate Coq loadpaths.
|
|
|
