| Age | Commit message (Collapse) | Author |
|---|
|
The field tactic post-processes the data generated during normalization
to ensure that vanished denominators do not cancel: essentially, this
step removes duplicates from a list of polynomials and uses the
clean list to generate the conjunction of associated non-zero conditions. This
conjunction is the proof obligation the user has to prove by hand after
a successful call to the field tactic.
The computation of the proof obligation statement
was performed using a fine-tuned reduction strategy, coded in
the newring.ml4 file (see the fv-protect tactic).
However, not only this strategy information was forgotten by the kernel,
but the strategy used at Qed time caused a real explosion (examples
normalized in 70s by the tactic have a one hour Qed). No idea why.
The fix consists in opacifying the part of the goal irrelevant to
computation and call the vm on the duplicate removal step. BTW this step
is programmed in a naive way and can probably be made more efficient.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Revised Coqtop.parse_args in a cleaner and lighter style
- Improved error message in case of argument parse failure:
* tell which option is expecting a related argument
* in case of unknown options, warn about them all at once
* do not hide the previous error messages by filling the
screen with usage(). Instead, suggest the use of --help.
- Specialized boolean config field Coq_config.arch_is_win32
- Faster Envars.coqlib, which is back to (unit->string), and
just access Flags.coqlib. Caveat: it must be initialized once
via Envars.set_coqlib
- Avoid keeping an opened channel to the "revision" file
- Direct load of theories/init/prelude.vo, no detour via Loadpath
Beware : ./configure must be runned after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Earlier, the elements of constr arrays were hash-consed, but not the
array itself. This helps a bit when the same (f a1 ... an) is manipulated
a lot : -20% in the size of opaque terms in Integral_domain.vo and Nsatz.vo
Similarly it's interesting to hash-cons sub-lists for dirpaths,
since in Coq.A.B and Coq.A.C we could share Coq.A.
With this patch, the hash-consing of constr seems quasi-optimal:
Pierre-Marie's marshal compactor is unable to shrink opaque tables by
more than 2%, and this difference seems to be due to untyped compaction
(for the compactor Rel 1 = Prop Pos).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16723 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This file should compile now twice as fast as earlier.
A large part of this speedup comes from swithching to
proofs without "auto" (and also improving them quite a lot).
Nicer lemma statements thanks to notations and
separate scopes (%ring, %coef, %poly).
The Field_correct lemma lost some args (sign_theory ...)
during the refactoring. After inspection, this looks legitimate,
so I've hack the field tactic accordingly. The args were there
probably due to some intuition or similar interfering with local
vars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It seems that it's critical for the native compiler that
a fresh (ref NotLinked) is created during substitution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16716 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Trying to understand if the edit concernes the processed zone
from the begin_user_action callback was a bad idea, the callback
cannot reliably know where the edit takes place (E.g. insert mark
means nothing: one can copy from the insert point but paste elsewhere).
The callbacks delete_range and insert_text do know where the edit is and
can ask coq to backtrack if needed. If coq is busy, the user action is
cancelled (the locked zone cannot be unlocked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Simple framework for remote counters. The slaves ask
the master for a fresh value. On the master the thread
manager answers with a bunch of fresh values (so that further
requests can be immediately satisfied).
Remote counters are guarded with a mutex on the master,
because all slave managers as well as the master thread
can access the counter at the same time.
I know the name sucks. These counters are remote for the slaves,
and local for the master. I'm open to suggestions...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The earlier type [struct_expr_body] was far too broad,
leading to code with unclear invariants, many "assert false", etc etc.
Its replacement [module_alg_expr] has only three constructors:
* MEident
* MEapply : note the module_path as 2nd arg, no more constraints here
* MEwith : no more constant_body inside, constr is just fine
But no more SEBfunctor or SEBstruct constructor here (see below).
This way, this datatype corresponds to algebraic expressions,
i.e. anything that can appear in non-interactive modules.
In fact, it even coincides now with [Entries.module_struct_entry].
- Functor constructors are now necessarily on top of other
structures thanks to a generic [functorize] datatype.
- Structures are now separated from algebraic expressions by design :
the [mod_type] and [typ_expr] fields now only contain structures
(or functorized structures), while [mod_type_alg] and [typ_expr_alg]
are restricted to algebraic expressions only.
- Only the implementation field [mod_expr] could be either algebraic
or structural. We handle this via a specialized datatype
[module_implementation] with four constructors:
* Abstract : no implementation (cf. for instance Declare Module)
* Algebraic(_) : for non-interactive modules, e.g. Module M := N.
* Struct(_) : for interactive module, e.g. Module M : T. ... End M.
* FullStruct : for interactive module with no type restriction.
The [FullStruct] is a particular case of [Struct] where the implementation
need not be stored at all, since it is exactly equal to its expanded
type present in [mod_type]. This is less fragile than hoping as earlier
that pointer equality between [mod_type] and [mod_expr] will be
preserved...
- We clearly emphasize that only [mod_type] and [typ_expr] are
relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
are there only for a nicer extraction and shorter module printing.
[mod_expr] is also not accessed by the kernel, but it is important
for Print Assumptions later.
- A few implicit invariants remain, for instance "no MEwith in mod_expr",
see the final comment in Declarations
- Heavy refactoring of module-related files : modops, mod_typing,
safe_typing, declaremods, extraction/extract_env.ml ...
- Coqchk has been adapted accordingly. The code concerning MEwith
in Mod_checking is now gone, since we cannot have any in mod_expr.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We try harder to preserve pointer equality when substituting.
This will probably have little effect (for instance the
constr_substituted are anyway _never_ substituted in place),
but it cannot harm.
Two particular cases:
- we try to share (and maintain shared) mind_user_lc and mind_nf_lc
- we try to share (and maintain shared) mod_expr and mod_type
TODO: check that native compiler is still ok, since we might have
less (ref NotLinked) now. Having references in constant_body and co
is anyway a Very Bad Idea (TM).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16709 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- No more modinfo sub-record in the safe_environment record,
this was a syntactic pain.
senv.modinfo.modpath --> senv.modpath
senv.modinfo.variant --> senv.modvariant
senv.modinfo.resolver --> senv.modresolver
senv.modinfo.resolver_of_param --> senv.paramresolver
senv.modinfo.label : removed (can be inferred from modpath)
- No more systematic chaining of safe_environment ('old' field).
Instead, earlier safe_environment is stored in the modvariant field
when necessary (STRUCT and SIG case).
- Improved sharing between end_module and end_modtype
- More qualified names instead of open, better comments, ...
- Some user errors are now checked earlier elsewhere (see for
instance vernac_end_segment), so we can turn these errors into
asserts. The user error about higher-order include is now algebraic.
- Highlight the idea of a state monad in Safe_typing :
type 'a safe_transformer = safe_environment -> 'a * safe_environment
More systematic code in Global, thanks to 'globalize' function.
- Declaremods : less informations stored in openmod_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Without this, the stdlib vo files are +30% larger
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16704 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
No semantic change, but way less debug printings
coming from Paral-ITP
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16703 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.
These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
That is pretty tricky, and is not as nice I would like
for to_process text (that is still considered as locked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I don't know why yet, but let's be conservative
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16697 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We need the proof object to continue (there is no real dependency
tracking so we assume we need it immediately).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16694 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This time all collateral effects of forcing the execution
of dropped proofs should be handled correctly
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16692 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
still not working, it complains about the universe constraint
set...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(this should have been the first commit of Paral-ITP)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16686 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
documentation available in the help menu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The warning output by vernacextend when the classifier is missing
is the documentation of this commit:
Warning: Vernac entry "Foo" misses a classifier. A classifier is a
function that returns an expression of type vernac_classification (see
Vernacexpr). You can:
- Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new
vernacular command does not alter the system state;
- Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new
vernacular command alters the system state but not the parser nor it starts
a proof or ends one;
- Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global
function f. The function f will be called passing "Foo" as the
only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one
classifier is called.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
