| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
As a result the use of the glist-style interface for manipulating goals has almost been removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
It was a bad idea. The new API based on lists seems more sensible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the compilation of Coq, we can see an increase of ~20% compile time on
my completely non-scientific tests. Hopefully this can be fixed.
There are a lot of low hanging fruits, but this is an iso-functionality commit.
With a few exceptions which were not necessary for the compilation of the theories:
- The declarative mode is not yet ported
- The timeout tactical is currently deactivated because it needs some subtle
I/O. The framework is ready to handle it, but I haven't done it yet.
- For much the same reason, the ltac debugger is unplugged. It will be more
difficult, but will eventually be back.
A few comments:
I occasionnally used a coercion from [unit Proofview.tactic] to the old
[Prooftype.tactic]. It should work smoothely, but loses any backtracking
information: the coerced tactics has at most one success.
- It is used in autorewrite (it shouldn't be a problem there). Autorewrite's
code is fairly old and tricky
- It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes
as we might want to have various success in a "Hint Extern". But it would
require a heavy port of eauto.ml4
- It is used in typeclass eauto, but with a little help from Matthieu, it should
be easy to port the whole thing to the new tactic engine, actually simplifying
the code.
- It is used in fourier. I believe it to be inocuous.
- It is used in firstorder and congruence. I think it's ok. Their code is
somewhat intricate and I'm not sure they would be easy to actually port.
- It is used heavily in Function. And honestly, I have no idea whether it can do
harm or not.
Updates:
(11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based
architecture for Ltac matching (r16533), which avoid painfully and expensively
working around the exception-throwing control flow of the previous API.
(11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730)
rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN
apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma,
rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially
tclREPEAT, causing rewrites to be tried in the side-conditions of conditional
rewrites as well). The new implementation makes Coq faster, but it is
pretty much impossible to tell if it is significant at all.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
state out of one we were threading all the way along. This should be
safer, as one cannot forego side effects accidentally by manipulating
explicitly the [sigma] container.
Still, this patch raised the issue of badly used evar maps. There
is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the
fact it uses evar maps in an unorthodox way.
Likewise, that mean we have to revert all contrib patches that added
effect threading...
There was also a dubious use of side effects in their toplevel handling,
that duplicates them, leading to the need of a rather unsafe List.uniquize
afterwards. It should be investigaged.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Btw, remove unused code in the xml plugin and in Tactic_printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
particular, new printer for evar_map which displays undefined evars +
defined evars that were instantiated by these undefined evars and
recursively, up to some arbitrary level n chosen to be in practice
n=2 (thanks to Arnaud).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
instead of the index required by the user; extended FixRule and
Cofix accordingly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 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@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
effacé dans un intro-pattern (suggéré par ssreflect).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
tombé au cours du temps
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
rename A into B, C into D, E into F.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
comportement pré-inductifs polymorphes vis à vis du test d'inclusion
des hypothèses de section (i.e. test dans le noyau mais pas dans
typing.ml qui est le typeur utilisé généralement par les
tactiques). En effet, les variables de section sont vues par les
tactiques comme des variables locales qui sont modifiables (p.ex. par
conversion). Mais le changement de la signature des variables de
section fait échouer le typage noyau (qui exige une égalité syntaxique
des types de ces variables) pour les demandes de typage en provenance
des tactiques.
Quelle est la bonne solution ?
- Faut-il comparer les variables de section modulo réduction dans le noyau ?
- Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section
pour les tactiques, comme c'était le cas avant les inductifs polymorphes
(c'est la solution pragmatique adoptée pour résoudre #1325)
- Faut-il éviter la confusion entre variables de section et variables de but ?
Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui,
outre des calculs de typage allégés pour les tactiques, évite aussi de
tomber sur le comportement du bug #1325.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
dans redexpr.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Tacmach
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
passent donc de Termops a Constrintern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
aspiwack
gareuselesinge
ppedrot
letouzey
regisgia
herbelin
pboutill
glondu
barras
gregoire