| Age | Commit message (Collapse) | Author |
|---|
|
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
|
|
on the contrary of message given in 23041481f, while it introduces a
square time complexity of the size of the goal in subterm finding.
|
|
|
|
|
|
|
|
The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
|
|
|
|
|
|
|
|
grammar.cma is built by Makefile.build in a specific, hardcoded way.
Let's remove this old .mllib file to avoid potential confusions in
the future.
|
|
For now, the pack name reuse the previous .cma name of the plugin,
(extraction_plugin, etc).
The earlier .mllib files in plugins are now named .mlpack.
They are also handled by bin/ocamllibdep, just as .mllib.
We've slightly modified ocamllibdep to help setting the -for-pack
options: in *.mlpack.d files, there are some extra variables such as
foo/bar_FORPACK := -for-pack Baz
when foo/bar.ml is mentioned in baz.mlpack.
When a plugin is calling a function from another plugin, the name
need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).
Btw, we discard the generated files plugins/*/*_mod.ml, they are
obsolete now, replaced by DECLARE PLUGIN.
Nota: there's a potential problem in the micromega directory,
some .ml files are linked both in micromega_plugin and in csdpcert.
And we now compile these files with a -for-pack, even if they are
not packed in the case of csdpcert. In practice, csdpcert seems
to work well, but we should verify with OCaml experts.
|
|
|
|
General idea : Makefile.build was far too big to be easy to grasp or
maintain, with information scattered everywhere. Let's try to tidy that!
Normally, this commit is transparent for the user. We simply regroup
some parts of Makefile.build in several new dedicated files:
- Makefile.ide
- Makefile.checker
- Makefile.dev (for printers, revision, extra partial targets, otags)
- Makefile.install
These new files are "included" at the start of Makefile.build, to provide
the same behavior as before, but with a Makefile.build shrinked by 50%
(to approx 600 lines). Makefile.build now handles in priority the build
of coqtop, minor tools, theories and plugins.
Note: this is *not* a separate build system for coqchk nor coqide,
even if this can be seen as a first step in this direction (won't be easy
anyway to continue, due to the sharing of various stuff in lib and more).
In particular Makefile.{coqchk,ide} may rely here and there on some generic
rules left in Mafefile.build. Conversely, be sure to prefix rules in
Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid
interferences with generic rules.
Makefile.common is still there, but quite simplified. For instance,
some variables that were used only once (e.g. lists of cmo files to link
in the various tools) are now defined in Makefile.build, directly
where they're needed. THEORIESVO and PLUGINSVO are made directly out of
the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual
list of subdirs anymore. Specific sub-targets such as 'reals' still
exist, but in Makefile.dev, and they aren't mandatory.
Makefile.doc is augmented by the rules building the documentation of
the sources via ocamldoc.
This classification attempt could probably be improved. For instance,
the install rules for coqide are currently in Makefile.ide, but could
also go in Makefile.install. Note that I've removed install-library-light
which was broken anyway (arith isn't self-contained anymore).
|
|
|
|
More precisely, we first remove *.native, *.cm*, *.o, which should
normally consistute the only content of these .coq-native directories,
and then remove these directories if they're indeed empty
|
|
It has been accidentaly broken since early 2014 (and especially
in 8.5), no easy repair, I won't devote any more hours to this stuff.
Moreover no one seems to care apart from Emilio, but he's ok to work
on this in a separate repository or branch.
I left a dev/doc/ocamlbuild.txt file with a few words about this
experiment.
|
|
|
|
|
|
|
|
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
|
|
There is little point in telling the user the error report is sub optimal.
In this particular case, such error has already been reported (on
the correct location) so reminding it in a non-localized way is not
even that bad.
|
|
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
|
|
|
|
|
|
|
|
|
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
|
|
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
and global for 8.4 and 8.5.
|
|
|
|
|
|
Since this is really what they are.
Squashing this renaming back to the root of the feature branch is hard.
|
|
By default we enable only {} and par: that are detectable in
a complete way.
|
|
Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
|
|
|
|
|
|
|
|
|
|
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
|
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
|
|
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
|
|
|
|
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
