| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Those macros used to handle in a special way the grammar entries and generic
arguments known statically from Coq, i.e. defined before Pcoq. This was hardly
predictible and very implementation-dependent.
We made the EXTEND macros much more light-weight by treating in a uniform way
all entries and arguments. Now, they are all produced by outputing the name
as-is for entries and as "wit_$name" for genargs, thus letting the scope
of the ML code decide which entrie is going to be taken. This is documented
in the dev/ changelog.
This also allows to get rid of a lot of dependencies in the grammar preprocessor,
reducing it to a small functional shell. It is still depending on Compat, but it
is most probably possible to reduce the code size even more.
|
|
|
|
|
|
This fixes parsing conflicts with the [fix ... with] tactic.
|
|
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
|
|
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
|
|
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
|
|
|
The regression was introduced by efa1c32a4d178, which replaced
unification by conversion when looking for more occurrences of a
subterm. The conversion function called was not the right one, as it
was not inferring constraints.
|
|
|
|
|
|
There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.
|
|
|
|
|
|
|
|
|
|
|
|
Due to a change in pretyping, using cast annotations as typing
constraints, the canonical structure problems given to the unification
could contain non-evar-normalized terms, hence we force
evar normalization where necessary to ensure the same CS solutions
can be found. Here the dependency test is fooled by an erasable
dependency, and the following resolution needs a independent codomain
for pop b to be well-scoped.
|
|
We protect Sys.readdir calls againts any nasty exception.
|
|
We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.
This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
|
|
The SIGINT sent to the master coqtop process was lost in a watchdog thread,
so that the STM resulted in an inconsistent state. This patch catches gracefully
the exception and kills the task as if it were normally cancelled. Note that
it probably won't work on non-POSIX architectures, but it does not really
matter because interrupt was already badly handled anyway.
|
|
|
|
Forcefully equating it to the inferred level is not always desirable or possible.
|
|
When generating the OS X Coq + CoqIDE bundle, hdiutil often produces error
5341. This seems to be a known bug on Apple's side, occurring for some sizes of
dmg files. We try to change the current (problematic) size by adding a file
full of random bits.
|
|
|
|
|
|
|
|
notations in patterns than in terms, wrt implicit arguments and
scopes.
See file Notations2.v for the conventions in use in terms.
Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).
There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).
|
|
|
|
arguments and scopes with abbreviations and notations.
Comments are welcome on the proposed solutions for uniformization.
|
|
|
|
|
|
|
|
So adding a test-suite file and closing the bug.
|
|
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
|
|
|
Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.
This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.
Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
|
|
aspiwack-render-prehistory3
Pull request #120
|
|
|
|
They were not parsed correctly with a newline in the middle.
|
|
It got lost during a merge with the 8.5 branch.
|
|
Add test-suite file to ensure non-regression.
|
|
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
|
|
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
|
|
|
|
|
|
|
|
|
|
