aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Fix native compute for byte compiled Coq.Gravatar Gaëtan Gilbert2017-11-28
|
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function.
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
|/ | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
* Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ | | | | | | constructs.
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | | | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* Merge PR #6058: Remove redundant env argument to Reduction.ccnvGravatar Maxime Dénès2017-11-15
|\
* | [ci] [coq] Complete 4.06.0 support.Gravatar Emilio Jesus Gallego Arias2017-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | Due to an API change in laglgtk, we need to update CoqIDE. We use a makefile hack so it can compile with lablgtk < 2.8.16, another option would be to require 2.8.16 as a minimal dependency. We also refactor travis to test more lablgtk versions. We also need to account for improved attribute handling in 4.06.0, in particular module aliases will propagate the deprecation status. Fixes #6140.
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | We do up to `Term` which is the main bulk of the changes.
* | [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | This will allow to merge back `Names` with `API.Names`
* | [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | | | | | This is a first step towards some of the solutions proposed in #6008.
| * Remove redundant env argument to Reduction.ccnvGravatar Gaëtan Gilbert2017-11-02
|/ | | | | The infos already contain the env. Note that it was only actually used in the 2 lookup_mind lines.
* A missing newline after a comment.Gravatar Hugo Herbelin2017-10-24
|
* Merge PR #1155: Use type nonrec in some functor arguments.Gravatar Maxime Dénès2017-10-20
|\
* | [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
| * Use type nonrec in some functor arguments.Gravatar Gaëtan Gilbert2017-10-16
|/
* Merge PR #1103: Take Suggest Proof Using outside the kernel.Gravatar Maxime Dénès2017-10-13
|\
| * Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
* | [flambda] [native] Pass `-Oclassic` to the native compiler.Gravatar Emilio Jesus Gallego Arias2017-10-10
|/ | | | | | This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired.
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
* | [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move toplevel/STM flags from `Flags` to their proper components; this ensures that low-level code doesn't depend on them, which was incorrect and source of many problems wrt the interfaces. Lower-level components should not be aware whether they are running in batch or interactive mode, but instead provide a functional interface. In particular: == Added flags == - `Safe_typing.allow_delayed_constants` Allow delayed constants in the kernel. - `Flags.record_aux_file` Output `Proof using` information from the kernel. - `System.trust_file_cache` Assume that the file system won't change during our run. == Deleted flags == - `Flags.compilation_mode` - `Flags.batch_mode` Additionally, we modify the STM entry point and `coqtop` to account for the needed state. Note that testing may be necessary and the number of combinations possible exceeds what the test-suite / regular use does. The next step is to fix the initialization problems [c.f. Bugzilla], which will require a larger rework of the STM interface.
| * Remove unused Failure catchGravatar Gaëtan Gilbert2017-09-29
| | | | | | | | | | Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can tell.
| * Remove some duplication between Typeops and Nativenorm.Gravatar Gaëtan Gilbert2017-09-29
| |
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
| * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
* | Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ | |/ |/|
* | Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #931: Parametrize module bodyGravatar Maxime Dénès2017-09-07
|\ \ \
| | * | Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
| |/ / |/| | | | | | | | | | | This should save a lot of useless reallocations and hashset crawling, which end up costing a lot.
* | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \ \
| | * | Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
| | | |
| | * | Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12).
* | | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \ \ | |_|/ / |/| | |
| | * | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |/ / |/| | | | | | | | (from module List).
| * | Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| | |
* | | Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
|/ / | | | | | | | | Indeed OCaml has a similar file and this conflicts, at least in debugger.
* | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | |
| | * kernel: bugfix in filter_stack_domain.Gravatar Matthieu Sozeau2017-07-26
| |/ | | | | | | It did not consider that the argument might be higher-order, e.g. [nat -> I].
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* | Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | This ought to ease the understanding of the code.
* | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | This was an easy to prove property that I somehow overlooked.
* | Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | This is actually useless, the code does not depend on the value of the entry for side-effects.
* | Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment.
* | More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants.
* | Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
| |
* | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 11:42:04 +0000