| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: Zimmi48
|
|
This behaviour happens as a sub-bug of #10169 for instance.
|
|
|
|
This commit also prefixes young_ptr and young_limit along the way, so as
to not rely on OCaml's compatibility layer. This is a gratuitous change,
since this code is only meant to be compiled with OCaml < 4.10 anyway.
|
|
|
|
|
|
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
|
|
We also factorize a few checks by returning an option when looking for
a potentially template universe.
|
|
Same as #11780 except that this part can be backported to v8.11.
|
|
|
|
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
effects
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
We take inspiration and code from the Evil plugin.
|
|
|
|
|
|
|
|
The current behaviour could be considered as sub-optimal, but it probably
doesn't matter in practice as this happens when serializing side-effects.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
"where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Only significant change is in gcd / lcm which now are typed in `Z.t`
|
|
constants.
Reviewed-by: herbelin
|
|
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: vbgl
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
|
|
|
|
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.
|
|
The current CoqIDE bindings include an invisible U+FE00 variation selector
immediately following a number of symbols. For example, \empty maps to
U+2205 U+FE00 (UTF-8 encoding E2 88 85 EF B8 80), where U+2205 is the
expected Unicode point for "EMPTY SET".
This variation selector is difficult to work with in CoqIDE. If some
notation is defined to expect a U+2205 symbol, then a U+2205 U+FE00
expression does not match that notation, even though it is visually
identical. As a concrete example, this makes it difficult to use CoqIDE
to type the U+2205 EMPTY SET symbol for use with Iris, which expects a
U+2205 without a U+FE00. Pressing "backspace" at the right point deletes
the U+FE00 variation selector, even though visually nothing appears to
happen, which is also confusing.
This commit removes the U+FE00 invisible variation selectors from any
symbols in the default bindings for CoqIDE (it appeared in 35 symbols
out of 1400+ symbols; I have no theory for why those 35 symbols were
special in this way). This change was generated using:
sed -e s,$(printf '\xef\xb8\x80'),,
|
|
`plugins` needs to be present to coq_makefile variables are properly
initialized.
|
