| Age | Commit message (Collapse) | Author |
|---|
|
- coq logo isn't destructed anymore
- Erase debug printers not implemented for new proofs
- ocamldoc compatible comments for pretyping/rawterm.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/ocamldoc/
old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)
"make clean" cleans dev/ocamldoc/ properly
wierd? calls of dependency graph generation leave unchanged
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This is a fairly large commit (around 140 files and 7000 lines of code
impacted), it will cause some troubles for sure (I've listed the know
regressions below, there is bound to be more).
At this state of developpement it brings few features to the user, as
the old tactics were
ported with no change. Changes are on the side of the developer mostly.
Here comes a list of the major changes. I will stay brief, but the code
is hopefully well documented so that it is reasonably easy to infer the
details from it.
Feature developer-side:
* Primitives for a "real" refine tactic (generating a goal for each
evar).
* Abstract type of tactics, goals and proofs
* Tactics can act on several goals (formally all the focused goals). An
interesting consequence of this is that the tactical (. ; [ . | ... ])
can be separated in two
tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for
this particular syntax). We can also imagine a tactic to reorder the
goals.
* Possibility for a tactic to pass a value to following tactics (a
typical example is
an intro function which tells the following tactics which name it
introduced).
* backtracking primitives for tactics (it is now possible to implement a
tactical '+'
with (a+b);c equivalent to (a;c+b;c) (itself equivalent to
(a;c||b;c)). This is a valuable
tool to implement tactics like "auto" without nowing of the
implementation of tactics.
* A notion of proof modes, which allows to dynamically change the parser
for tactics. It is controlled at user level with the keywords Set
Default Proof Mode (this is the proof mode which is loaded at the start
of each proof) and Proof Mode (switches the proof mode of the current
proof) to control them.
* A new primitive Evd.fold_undefined which operates like an Evd.fold,
except it only goes through the evars whose body is Evar_empty. This is
a common operation throughout the code,
some of the fold-and-test-if-empty occurences have been replaced by
fold_undefined. For now,
it is only implemented as a fold-and-test, but we expect to have some
optimisations coming some day, as there can be a lot of evars in an
evar_map with this new implementation (I've observed a couple of
thousands), whereas there are rarely more than a dozen undefined ones.
Folding being a linear operation, this might result in a significant
speed-up.
* The declarative mode has been moved into the plugins. This is made
possible by the proof mode feature. I tried to document it so that it
can serve as a tutorial for a tactic mode plugin.
Features user-side:
* Unfocus does not go back to the root of the proof if several Focus-s
have been performed.
It only goes back to the point where it was last focused.
* experimental (non-documented) support of keywords
BeginSubproof/EndSubproof:
BeginSubproof focuses on first goal, one can unfocus only with
EndSubproof, and only
if the proof is completed for that goal.
* experimental (non-documented) support for bullets ('+', '-' and '*')
they act as hierarchical BeginSubproof/EndSubproof:
First time one uses '+' (for instance) it focuses on first goal, when
the subproof is
completed, one can use '+' again which unfocuses and focuses on next
first goal.
Meanwhile, one cas use '*' (for instance) to focus more deeply.
Known regressions:
* The xml plugin had some functions related to proof trees. As the
structure of proof changed significantly, they do not work anymore.
* I do not know how to implement info or show script in this new engine.
Actually I don't even know what they were suppose to actually mean in
earlier versions either. I wager they would require some calm thinking
before going back to work.
* Declarative mode not entirely working (in particular proofs by
induction need to be restored).
* A bug in the inversion tactic (observed in some contributions)
* A bug in Program (observed in some contributions)
* Minor change in the 'old' type of tactics causing some contributions
to fail.
* Compilation time takes about 10-15% longer for unknown reasons (I
suspect it might be linked to the fact that I don't perform any
reduction at QED-s, and also to some linear operations on evar_map-s
(see Evd.fold_undefined above)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ML names
(late consequences of commit r12603)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to rawconstr
Also cleaned a bit typing.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/doc/build*.txt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
*.dep.ps for svn
the syntax for find is sooo intuitive ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As pointed out by Nima Hoda, bash is not installed everywhere... and
we really don't NEED bash anyway.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12655 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* Unicodetable: Update with the standard table for lower case conversion.
* Util: Rewrite "lowercase_unicode" to take the entire unicode character set
into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(This should be a conservative extension of the old version.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- New (modular) mergesort purely using structural recursion
- Move of the (complex) notion of permutation up to setoid equality
formerly defined in Permutation.v to file PermutSetoid.v
- Re-use of the file Permutation.v for making the canonical notion
of permutation that was in List.v more visible
- New file Sorted.v that contains two definitions of sorted:
"Sorted" is a renaming of "sort" that was defined in file
Sorting.v and "StronglySorted" is the intuitive notion of sorted
(there is also LocallySorted which is a variant of Sorted)
- File Sorting.v is replaced by a call to the main Require of the directory
- The merge function whose specification rely on counting elements is moved
to Heap.v and both are stamped deprecated (the sort defined in
Heap.v has complexity n^2 in worst case)
- Added some new naming conventions
- Removed uselessly-maximal implicit arguments of Forall2 predicate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It has moved to the contribs (Sophia-Antipolis/Interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of objects having the same name as the section).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
same type is already registered.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12482 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).
Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in Relation_Operators.v and Operators_Properties.v more uniform in
general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
proposition de nommage standardisé des lemmes dans le trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12282 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in commit r12265. Add a few synonyms back in Libnames/Nameops to
maintain some minimal compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
revised-theories branch. The V5.10 period at Lyon is still unclear.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12138 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(bug 2092 and decl_mode.v in test suite).
- Added a debugging printer for pftreestate.
- Fixing American spelling in RefMan-decl.tex.
- Optimizing application of tactic validation by removing consistency
test in descend.
- Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
uglily to be factorized by hand.
- Typography in RefMan-tac.tex.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Adding test file related to commit 12080 (bug #2091).
- Cleaning old parsing stuff from 8.0.
- Support for camlp5 in base_include.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(tested on MacOS 10.5).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11990 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11929 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
