aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ↵Matthieu Sozeau
test-suite pass.
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle * Having a file named toplevel/toplevel.ml isn't a good idea when we also have a toplevel/toplevel.mllib that ought to produce a toplevel.cma. We rename toplevel.ml into Coqloop.ml * Extra cleanup of toplevel.mllib : - Ppextra isn't anywhere around (?!) - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway - Vernacexpr is a .mli and shouldn't appear in an .mllib * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml) * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread for coqchk).
2013-12-15Do not overallocate closures' named environments in infos. Modifying the accessPierre-Marie Pédrot
function is sufficient to skip the undefined variables.
2013-11-27Reduction: every n iterations a slaves process checks for interruptionEnrico Tassi
I chose n to be 10000 iterations. It might be big, but a slave, to check for a termination request, has to pass the ball to the thread that sends "regularly" Ticks to the master process. Thread.yield is a system call, so we have to do it very rarely.
2013-11-24Slightly more efficient zip function in Closure.Pierre-Marie Pédrot
2013-11-23Small allocation improvement in Closure.Pierre-Marie Pédrot
2013-11-15Revert "Fast lookup_named in environments, based on maps instead of lists."ppedrot
Contrarily to my machine results, it seems that it tore down the performance of Coq on benchmarks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-13Fast lookup_named in environments, based on maps instead of lists.ppedrot
This was quite a severe performance bottleneck. Ideally, this data structure should be put into contexts, but the relevant type is transparent... For now, we stick to this inelegant workaround. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17086 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Using allocation-free version of Array higher-order function in criticalppedrot
cases, which are precisely term manipulation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17054 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Evar module now uses default Int maps and sets.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17049 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Closure: fix an issue with r16959 spotted by Matthieuletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16966 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)letouzey
This commit should fix the contrib ProjectiveGeometry This update_delta_resolver is in fact a sequential composition (resolver1 then resolver2). The earlier version was strangely favoring the bindings coming from resolver2 over the bindings coming from (resolver1 chained with resolver2). So any inlining information stored in resolver1 could be discarded savagely. Apparently, this situation wasn't occurring in practice until recently, when I started to do lots of Mod_subst.join for improving the size of modular libobjects in the vo's. So, when combining two resolvers now : - Inline(_,None) is the weakest information, it's just a declaration that we intend to inline this kn someday if possible (i.e. when we'll have a transparent implementation for it). This kind of Inline is only relevant inside a module type. - Equiv(_) should only appear in modules (after some Include) so it should be ok if it takes precedence over any Inline(_,None) remaining in the other resolver. - Inline(_,Some _) is there after functor application (cf inline_delta_resolver) : we've done the inlining, so we don't care anymore about other Equiv(_) or Inline(_,None) informations about this kn, since we have anyway a new body for it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16965 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Fixing Kerpair.hash. Since the beginning, it dit not respect the typeppedrot
equality, maybe impeding hashconsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16964 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
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
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
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
2013-10-31Avoiding useless allocations in Closure.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16959 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Allocation-friendly version of [Pre_env.push_named].ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16947 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Optimizing universes: tail-rec, allocation friendly [compare_leq].ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16946 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-28Native compiler: library compilation errors are now non fatal.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-27More sharing in Constr.map_with_binders.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16938 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
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
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16935 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Rtree : cleanup of the comparing codeletouzey
* Using generic fold functions was unecessarily obscure * No more List.mem and hence indirect use of ocaml generic comparison * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic semantic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Specializing hash functions for widely used types.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24Turn many List.assoc into List.assoc_fletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList.index is now cList.index_f, same for index0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23Optimizing Vars.replace_varsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16916 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Removing some generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Various optimizations in Constr, such as term sharing and allocationppedrot
avoiding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
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
2013-10-04Fix comment for new string syntax (OCaml trunk).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03A shallow copy of a pre_env does not contain the vm cachegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
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
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30ind_tables: properly handling side effectsgareuselesinge
If a constant is defined as transparent, not only its side effects (opaque sub proofs as in abstract, and transparent ind schemes) are declared globally, but the ones that are schemes are also declared as such. The only sub optimal thing is that the code handling in a special way the side effects of transparent constants is in declare.ml that does not see ind_tables.ml, hence a forward ref to a function is used. IMO, ind_tables has no reason to stay in toplevel/. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-30Remove Obj.magic from safe typinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Replacing lists by sets in clear tactic.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16734 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-23Fix computation of discharged hyps for inductive types forgetting the ↵msozeau
conclusion of the arity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16732 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- 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
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
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
2013-08-20Partial revert of r16711letouzey
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
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
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
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 05:29:37 +0000