| 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.
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
(inconsistencies in parsing/printing notations to partial applications)
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Reviewed-by: jfehrle
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
to control uniform parameters.
This replaces the attribute.
|
|
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
|
|
If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
the subentry
- if in constr, it is 200 by convention
If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
SELF, a NEXT, or (if on the right) a LEVEL
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Parameters)
Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:
- not used in the main build since a long time
- not tested
- not kept up to date with upstream
This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.
`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.
We also remove the residual `-slash` option.
|
|
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
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
Reviewed-by: gares
|
|
This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)
It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.
|
|
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
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
|
|
|
