| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \
| | |
| | |
| | | |
failure in other file
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
Instead of the current hack that won't work as soon as we check some
part of the document asynchronously, we make the warning processor
recover a proper location if the warning doesn't have one attached.
This is what CoqIDE does [but it queries it's own document model].
Fixes: #6172
|
| | | |
|
| | |
| |
| |
| |
| | |
I make here a minimal fix, but a lot of cleaning should be done around
Aux_file handling, including removing some code from the kernel.
|
| |/
|
|
|
|
| |
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.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
fiat-crypto/OSX
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| | |
Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.
PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.
|
| | |
| |
| |
| | |
Note that we don't look inside -arg for eg -coqlib.
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
| | |/ |
|
| |/
|
|
| |
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.
This code was written by Benjamin Grégoire and myself.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
camlp4
|
| | | |
| | |
| | |
| | | |
longer use camlp4.
|
| | |/
|/| |
|
| |/
|
|
|
|
|
|
|
|
| |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The old semantics of `with/without_option` allowed the called function
to modify the value of the option. This is an issue mainly with the
`silently/verbose` combinators, as `Set Silent` can be executed under
one of them and thus the modification will be lost in the updated code
introduced in a554519874c15d0a790082e5f15f3dc2419c6c38
IMHO these kind of semantics are quite messy but we have to preserve
them in order for the `Silent` system to work. In fact, note that in
the previous code, `with_options` was not consistent with
`with_option` [maybe that got me confused?]
Ideally we could restore the saner semantics once we clean up the
`Silent` system [that is, we remove the flag altogether], but that'll
have to wait.
Fixes #6645.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| | |/
|/|
| |
| |
| |
| | |
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
| |\ \
| | |
| | |
| | | |
possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
|
| | | |
| | |
| | |
| | | |
One less global flag.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
| | |
| |
| |
| | |
This was apparently either silently doing nothing or failing.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
same right-hand side.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
These are convenient to use `command.ml` for example.
We also fix a critical bug in the `fold_left_map` family of functions,
as witnessed by this old behavior.
```ocaml
fold_left2_map (fun c u v -> c+1,u+v) 0 [1;2;3] [1;2;3;];;
- : int * int list = (3, [6; 4; 2])
```
I have opted for a simple fix keeping the tail-recursive nature, I am
not in the mood of writing base libraries, but feel free to improve.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Adding a space before the bar separating disjunctive patterns.
Removing an extra space after the bar for inner disjunctive patterns.
|
| | | | |/ / /
| | | | | |
| | | | | |
| | | | | | |
And some code simplification.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
| | | |/ / /
| |/| | |
| | | | |
| | | | |
| | | | | |
This brings us one step closer to actually moving all STM flags to
`stm`.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| | |/ / /
| | | |
| | | |
| | | |
| | | | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |/ / / |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
Maxime Dénès
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Hugo Herbelin
Gaëtan Gilbert
mrmr1993
Théo Zimmermann
Jim Fehrle
Enrico Tassi
Paul Steckler