aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Fix exponential behavior in native compiler with retroknowledge.Gravatar Maxime Dénès2014-04-09
|
* Fix name of some Int31 operations in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
| | | | applications of I31 constructor as lazy.
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
|
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
| | | | | This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
|
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
| | | | dependencies.
* Int31 literals in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Uint31 support.Gravatar Maxime Dénès2014-04-09
|
* Fix universe handling (bug introduced in vi2vo commit)Gravatar Enrico Tassi2014-04-08
| | | | | | | | | | Inside a section, Let followed by a Proof. Qed. are handled as regular definitions, hence they have universe constraints coming from the type and from the body. Only the former set was returned to libstack, but both sets were added to the global universe graph. Hence, at section closing time, an incomplete set of universe constraints was added back to the global graph (End Section replays the libstack) and hence saved in the .vo file. coqchk was right in reporting missing constraints.
* Fixing coqchk. It was my fault, I misused canonical and user equalitiesGravatar Pierre-Marie Pédrot2014-04-04
| | | | | when defining cache hash tables in Closure. Why it was working in 3.12 is a mystery to me.
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
|
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
| | | | transparent status of variables and constants.
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
| | | | no particular purpose.
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
| | | | | | | | | | | | | | | | | | Universes that are computed in the vi2vo step are not part of the outermost module stocked in the vo file. They are part of the Library.seg_univ segment and are hence added to the safe env when the vo file is loaded. The seg_univ has been augmented. It is now: - an array of universe constraints, one for each constant whose opaque body was computed in the vi2vo phase. This is useful only to print the constants (and its associated constraints). - a union of all the constraints that come from proofs generated in the vi2vo phase. This is morally the missing bits in the toplevel module body stocked in the vo file, and is there to ease the loading of a .vo file (obtained from a .vi file). - a boolean, false if the file is incomplete (.vi) and true if it is complete (.vo obtained via vi2vo).
* Fix (3243): univ constraints of module subtyping were not propagatedGravatar Enrico Tassi2014-03-11
| | | | | | | Universe constraints coming from subtyping were not propagated to the outermost module and hence not stocked in the .vo file. Still, they were added to the interactive safe environment and hence checked for satisfiability.
* Useless Array.to_list in Typeops.Gravatar Pierre-Marie Pédrot2014-03-10
|
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
|
* Also use HMaps in KNmap.Gravatar Pierre-Marie Pédrot2014-03-08
|
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
| | | | iter order, but it seems nobody was relying on it (contrarily to the string case).
* Inductive maps in Environ now use HMap.Gravatar Pierre-Marie Pédrot2014-03-06
|
* Fix typo in comment.Gravatar Maxime Dénès2014-03-05
|
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
|
* Lazily computed hash in KerName.t.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
| | | | The removed code isn't used locally and isn't exported in the signature
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Correct handling of hashconsing of constraint sets. The previous implementationGravatar Pierre-Marie Pédrot2014-03-05
| | | | did not respect the requirement that equality should preserve hash.
* Fixing pervasives equalities in Vconv.Gravatar Pierre-Marie Pédrot2014-03-04
|
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
| | | | | | duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite.
* Removing generic hashes in kernel.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Kernel names are implemented using records.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
|
* Hunting pervasive equality in native compiler. It seems they were used forGravatar Pierre-Marie Pédrot2014-03-01
| | | | | optimization purposes. I replaced their use with the under-approximation of pointer equality.
* STM: when batch compiling a vo, assert we behave conservativelyGravatar Enrico Tassi2014-02-26
| | | | | This meas that the list of future_constraints in safe_env is empty, meaning that nothing was delayed.
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
| | | | | When you resume the compilation of a .vi file, you want to avoid collisions on fresh names.
* univ: removing dead codeGravatar Enrico Tassi2014-02-26
|
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To obtain a.vo one can now: 1) coqtop -quick -compile a 2) coqtop -vi2vo a.vi To make that possible the .vo structure has been complicated. It is now made of 5 segments. | vo | vi | vi2vo | contents --------------+------+-----+-------+------------------------------------ lib | Yes | Yes | Yes | libstack (modules, notations,...) opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs discharge | No | Yes | No | data needed to close sections tasks | No | Yes | No | STM tasks to produce proof terms opaque_proofs | Yes | Yes | Yes | proof terms --------------+------+-----+-------+------------------------------------ This means one can load only the strictly necessay parts. Usually one does not load the tasks segment of a .vi nor the opaque_proof segment of a .vo, unless one is turning a .vi into a .vo, in which case he load all the segments. Optional segments are marshalled as None. But for lib, all segments are Array.t of: | type --------------+--------------------------------------------------------- lib | a list of Libobject.obj (n'importe quoi) opauqe_univs | Univ.consraints Future.computation discharge | what Cooking.cook_constr needs tasks | Stm.tasks (a task is system_state * vernacexpr list) opaque_proofs | Term.constr Future.computation --------------+------+-----+-------+------------------------------------ Invariant: all Future.computation in a vo file (obtained by a vi2vo compilation or not) have been terminated with Future.join (or Future.sink). This means they are values (inside a box). This invariant does not hold for vi files. E.g. opauqe_proofs can be dangling Future.computation (i.e. NotHere exception). The vi2vo compilation step will replace them by true values. Rationale for opaque_univs: in the vi2vo transformation we want to reuse the lib segment. Hence the missing pieces have to be put on the side, not inside. Opaque proof terms are already in a separte segment. Universe constraints are not, hence the new opauqe_univs segment. Such segment, if present in a .vo file, is always loaded, and Declare.open_constant will add to the environment the constraints stored there. For regular constants this is not necessay since the constraints are already in their enclosing module (and also in the constant_body). With vi2vo the constraints coming from the proof are not in the constant_body (hence not in the enclosing module) but there and are added to the environment explicitly by Declare.open_constant. Rationale for discharge: vi2vo produces a proof term in its original context (in the middle of a section). Then it has to discharge the object. This segment contains the data that is needed in order to do so. It is morally the input that Lib.close_section passes to Cooking (via the insane rewinding of libstack, GlobalRecipe, etc chain). Checksums: the checksum of .vi and a .vo obtain from it is the same. This means that if if b.vo has been compiled using a.vi, and then a.vi is compiled into a.vo, Require Import b works (and recursively loads a.vo).
* Optimization in kernel/vars.ml: directly allocate a fixed-size block in theGravatar Pierre-Marie Pédrot2014-02-20
| | | | subst1 case.
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
|
* Small optimizations in Closure:Gravatar Pierre-Marie Pédrot2014-02-09
| | | | | 1. Only apply last Zupdates 2. Better smartmap with state.
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
| | | | | | | I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed.
* Christmas is over...Gravatar Maxime Dénès2014-01-15
|
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
| | | | | | | Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:11:00 +0000