| Age | Commit message (Collapse) | Author |
|---|
|
all:tac applies tac to all the focused subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by extraction.
The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.
With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.
Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.
Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).
A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.
Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It doesn't matter much, it's simply a matter of aesthetic, so that all functions
in the interface of [Monads.IO] are pure ([IO.run] being the only impure
function but it's not part of the generic interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16974 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It now uses the same algorithm as pretyping does.
This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.
The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It allowed to restore the timeout tactics. It also prepares for the debugging
mechanism to be restored.
['a IO.t] is just [unit -> 'a].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 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
|
|
It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than
at each tclTHEN. Hopefully avoiding making things a bit less slow.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16968 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
|
|
This optimization was undone because the kernel type checking was
not a pure functions (it was accessing the conv_oracle state imperatively).
Now that the conv_oracle state is part of env, the optimization can be
restored. This was the cause of the increase in memory consumption, since
it was forcing to keep a copy of the system state for every proof, even the
ones that are not delayed/delegated to slaves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16941 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ideally, any component of the global state that is a function or any
other unmarshallable data should be stocked as an ephemeron to make
the state always marshallable.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
related code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
casts of ints to evars.
- 2 in Evarutil and Goal which are really needed, even though the Goal
one could (and should) be removed;
- 2 in G_xml and Detyping that are there for completeness sake, but
that might be made anomalies altogether;
- 1 in Newring which is quite dubious at best, and should be fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ultimately all evars should be created with respect to a given
evar map, instead of using a global counter.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unsatisfactory as some functions implicitly require some ordering
on the evars, but this is already better.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
safe_typing is not purely functional, hence we cannot chain it
as if it was a pure computation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It can be:
`Yes Full data, in a state that can be marshalled
`No Full data, good for Undo only
`Shallow Partial data, marshallable, good for slave processes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 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
|
|
of tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16567 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16559 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16535 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Clarification of the existence of three algorithms for solving
unconstrained evars:
- the type-class mechanism
- the heuristics for solving pending conversion problems and multi-candidates
- Declare Implicit Tactic (when called from tactics)
Main function for solving unconstrained evars (when not using
understand): Pretyping.solve_remaining_evars
- Clarification of the existence of three corresponding kinds of
errors when reporting about unsolved evars:
Main function for checking resolution of evars independently of the
understand functions: Pretyping.check_evars_are_solved
- Introduction of inference flags in pretyping for governing which
combination of the algorithms to use when calling some understand
function; there is also a flag of expanding or not evars and for
requiring or not the resolution of all evars
- Less hackish way of managing Pretyping.type_constraint: all three
different possibilities are now represented by three different
constructors
- Main semantical changes done:
- solving unconstrained evars and reporting is not any longer mixed:
one first tries to find unconstrained evars by any way possible;
one eventually reports on the existence of unsolved evars using
check_evars_are_solved
- checking unsolved evars is now done by looking at the evar map,
not by looking at the evars occurring in the terms to pretype; the
only observed consequence so far is in Cases.v because of subterms
(surprisingly) disappering after compilation of pattern-matching
- the API changed, see dev/doc/changes.txt
Still to do:
- Find more uniform naming schemes:
- for distinguishing when sigma is passed as a reference or as a value
(are used: suffix _evars, prefix e_)
- for distinguishing when evars are allowed to remain uninstantiated or not
(are used: suffix _evars, again, suffix _tcc, infix _open_)
- be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
"preinfer", or "pretype". Grammatically, "understanding a term" looks
strange.
- Investigate whether the inference flags in tacinterp.ml are really
what we want (e.g. do we really want that heuristic remains
activated when typeclasses are explicitly deactivated, idem in
Tacinterp.interp_open_constr where flags are strange).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1. sorts.ml: A small file utility for sorts;
2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;
3. vars.ml: Everything related to term variables, that is, occurences
and substitution;
4. context.ml: Rel/Named context and all that;
5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
