| Age | Commit message (Collapse) | Author |
|---|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
|
|
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
|
|
|
|
|
|
|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
The parsing rules defining classes of lexemes in language
configuration expect a Coq document and are not relevant in the
message and proof window. Thus backtracking on this part of #12169.
Keeping the highlighting style though.
|
|
This hopefully fix the segfaults we observe with completion.
|
|
Reviewed-by: ppedrot
|
|
It was previously only applied to the script buffer.
|
|
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
The iterator of the completion context does not seem trustable.
|
|
Let's see if it fixes #11943. See there for explanations about the
related segfault.
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
The completion proposals need to be ordered by length first for usability.
I aknowledge that it's too easy to mess up when refactoring, but here there was
a clear comment that this change should not have been performed.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
This is at least to be able to use spaces in file names (#11595).
In practice it protects also \, ', ", and many other symbols.
|
|
This encodes/decodes a list of string into a string in a way
compatible with shell interpretation. On the contrary of
Filename.quote which is for computer consumption, it introduces quotes
for human consumption.
The strategy is to split each string into substrings separated by
simple quotes. Each substring is surrounted by single quotes if it
contains a space. Otherwise, each backslash in the substring is
doubled. The substrings are concatenated separated by
backslash-protected single quote. The strings are then concatenated
separated with spaces. The decoding is shell-like in the sense that it
follows the rules of single quote, backslash and space.
|
|
|
|
This behaviour happens as a sub-bug of #10169 for instance.
|
|
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.
|
|
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'),,
|
|
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`.
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
Reviewed-by: ejgallego
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
