aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2019-04-30[vm] Backport from OCamlPierre Roux
Backport https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6 and https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e from OCaml VM
2019-04-30[vm] PPC64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785 from OCaml VM
2019-04-30[vm] ARM registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928 from OCaml VM
2019-04-30[vm] Arm 64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f from OCaml VM
2019-04-30[vm] x86_64 registersPierre Roux
Backport https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376 from OCaml VM
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-15[vm] Protect accu and coq_envPierre Roux
Protect accu and coq_env against GC calls in the VM when calling primitive integer functions on 32 bits architecture.
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
This is a step towards unifying the higher level ILs of the native and bytecode compilers. See https://github.com/coq/coq/projects/17
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp ↵Pierre-Marie Pédrot
skip_pattern Reviewed-by: ppedrot
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
This is convenient for the bootstrap of `coqdep`
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on ↵Gaëtan Gilbert
applications Reviewed-by: SkySkimmer
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
This fixes an incompleteness of subtyping on cumulative inductives, where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation depending on the variance of I's universe.
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
This takes advantage of the mutability of the fconstr relevance mark.
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-03-01[Kernel] Simpler generation of opcode filesVincent Laporte
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing.
2019-03-01write_uint63.ml: add headerVincent Laporte
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker.
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25[kernel] termination checking backtracks on stuck primitive projectionEnrico Tassi
2019-02-25[kernel] termination checking backtracks on stuck fixEnrico Tassi
2019-02-22[kernel] termination checking backtracks on stuck caseEnrico Tassi
The strategy is to backtrack when a constant is in head position: we first try to see if the arguments are guarded, if not we unfold. Since `Case` is represented as a head (rather than as a context as the reduction machine does) we did not backtrack there and reduce (including delta) the scrutinized in order to fire the iota redex. This commit adds a choice point in that specific case, and reduces eagerly (not step by step) the scrutinized in case of failure.
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
I think the usage looks cleaner this way.
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive ↵Pierre-Marie Pédrot
records Reviewed-by: ppedrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
In order for Dune to work in Windows we need to tweak some script calls, they need a POSIX shell and the `(run ...)` / `(system ...)` actions use `cmd.exe` on Windows. Hopefully, we will rely less on `bash` when Dune can understand Coq libraries. This affects shell scripts in `kernel/**.sh` for example. It is interesting to see how faster the Coq Windows build is with Dune + Windows. There are some problems with PATHs that prevent the test suite from working, these will be fixed in a future PR.
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-05 16:27:02 +0000