aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-30Merge PR #13958: [recordops] complete API rewrite; the module is now called ↵Pierre-Marie Pédrot
[structures] Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: herbelin Reviewed-by: ppedrot
2021-03-30CI: don't output-syncGaëtan Gilbert
Not much benefit and it breaks make's print-directory system.
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
Fixes #10704
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary ↵coqbot-app[bot]
dependencies: Le, Gt, Minus, Lt, Setoid Reviewed-by: anton-trunov
2021-03-29Merge PR #14025: [coqdep] remove leftover Caml stuff from man pagecoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-29Print type of offending expression in Ltac2 not-unit warning.Pierre-Marie Pédrot
Partial fix of #14013.
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
Dependencies for Caml files was removed in PR #11589, but some parts of it survived in the man page.
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
The documentation of extraction became outdated when the big.ml wrapper got modified by 094e4649c29e2426daca0476c140439de901dafe.
2021-03-26Merge PR #11907: [zify] attempt to speed up look up of constrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-03-26[doc] cleanup pretyping/structures.mliEnrico Tassi
2021-03-26Add non-performance-based testJason Gross
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented. Fixes #13996: missing Ltac1.to_ident.
2021-03-26[ci] overlay file for #13958Enrico Tassi
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-26Document as critical.Guillaume Melquiond
2021-03-26Be more thorough when testing PArray.set.Guillaume Melquiond
2021-03-26Improve dump of primitive OCaml operations.Guillaume Melquiond
2021-03-26Support OCaml primitives with an actual arity larger than 4.Guillaume Melquiond
PArray.set has arity 4, but due to the polymorphic universe, its actual arity is 5. As a consequence, Kshort_apply cannot be used to invoke it (or rather its accumulating version). Using Kapply does not quite work here, because Kpush_retaddr would have to be invoked before the arguments, that is, before we even know whether the arguments are accumulators. So, to use Kapply, one would need to push the return address, push duplicates of the already computed arguments, call the accumulator, and then pop the original arguments. This commit follows a simpler approach, but more restrictive, as it is still limited to arity 4, but this time independently from universes. To do so, the call is performed in two steps. First, a closure containing the universes is created. Second, the actual application to the original arguments is performed, for which Kshort_apply is sufficient. So, this is inefficient, because a closure is created just so that it can be immediately fully applied. But since this is the accumulator slow path, this does not matter.
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments.
2021-03-26Fix assertion that checks that APPLY can only be passed 4 arguments.Guillaume Melquiond
2021-03-26Split the return type away from the signature of primitive operations.Guillaume Melquiond
This avoids having to drop the last element of the signature in the common case.
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
Reviewed-by: silene
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26Similar fix for native compilation.Pierre-Marie Pédrot
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
Bytecode execution of persistent arrays can modify structured values meant to be marshalled in vo files. Some VM values are not marshallable, leading to this anomaly. There are further issues with the use of a hash table to store structured values, since they rely on structural equality and hashing functions. Persistent arrays are not safe in this context. Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
Reviewed-by: olaure01
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]
Reviewed-by: gares
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths ↵coqbot-app[bot]
to check for conversion Reviewed-by: gares Ack-by: SkySkimmer
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-26Expose less interface in coercionops.mliKazuhiko Sakaguchi
2021-03-25Merge PR #13988: Mention label name in signature mismatch error when ↵Pierre-Marie Pédrot
constant expected Reviewed-by: ppedrot
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
Fixes #14003: Ltac2 redefinition check is broken.
2021-03-25Merge PR #13989: fix documentation of Ltac2.Env.expandPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2021-03-24Merge PR #13993: iris_string_ident is no longer neededcoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-24Merge PR #13994: CI Quickchick: don't install quickchick executable to opamcoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-24CI Quickchick: don't install quickchick executable to opamGaëtan Gilbert
2021-03-24iris_string_ident is no longer neededRalf Jung
2021-03-24Merge PR #13981: Fix debug printersPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
Fix #13987
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-24Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ↵Pierre-Marie Pédrot
stack. Reviewed-by: ppedrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:05:26 +0000