aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
Issue #10603
2019-12-17Merge PR #11299: [VM] fix volatile declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as ↵Maxime Dénès
non-resolvable, always Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-17Merge PR #11294: Advertise doc for master branch in README.Maxime Dénès
Reviewed-by: maximedenes
2019-12-16Merge PR #11291: Being explicit on existence of a remote link in stdlib to ↵Théo Zimmermann
avoid possible "breach of privacy" Reviewed-by: Zimmi48
2019-12-16Advertise doc for master branch in README.Théo Zimmermann
2019-12-16Merge PR #10695: [ci] [dune] Updates to dune builds artifacts.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2019-12-16[make] Add _build_boot to find_skip_dirsEmilio Jesus Gallego Arias
2019-12-16[dune] Use a special directory for the boot buildEmilio Jesus Gallego Arias
This is related to and fixes #10694 in part. When calling bootstrap in an incremental build step, we must be sure the generated dune files are in place. In the CI, these won't be in place, so we must bootstrap without altering the digest and trace database coming from the artifact. Using a separate boot step to recreate the missing `dune` files works fine and takes just a few seconds.
2019-12-16[ci] [dune] Updates to dune builds artifacts.Emilio Jesus Gallego Arias
Closes #10694 We modify handling of artifacts for dune builds: - we preserve `_build/log` log as artifact for ci-builds, - we use a tar.gz as to preserve file permissions which is necessary in order to reuse the artifacts in an incremental build. Dune uses this rule to digest a file: ``` Digest.generic (file_contents f, f.stats.st_perm land 0o100 (* Only take USR_X in account *)) ``` Since a few releases, Gitlab CI uses `.zip` as the storage format for artifacts, this means that files in `_build` will get the executable bit set when they did not have it originally, making all the digest cache to miss. This caused #10694 . See https://gitlab.com/gitlab-org/gitlab/issues/18711
2019-12-14Being explicit on existence of a remote link.Hugo Herbelin
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
2019-12-14Merge PR #11251: [micromega] reformating using ocamlformatMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵Théo Zimmermann
INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle
2019-12-13Merge PR #11257: [dev] [ocaml] Add ocamlformat configuration.Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-13Add ocamlformat dependency to Nix fileMaxime Dénès
2019-12-13Merge PR #11283: Split up stdlib install command (too long)Maxime Dénès
Reviewed-by: maximedenes
2019-12-13[build] Allow the selection of build system using an env var.Emilio Jesus Gallego Arias
This is undocumented on purpose by now. Suggested by Gaëtan Gilbert
2019-12-13[doc] [INSTALL] split make-based install instructions to its own file.Emilio Jesus Gallego Arias
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-13[make] Rename Makefile to Makefile.makeEmilio Jesus Gallego Arias
Picked from #8729. This should help preserve the history better when we split.
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0.
2019-12-13[ci] [docker] Install ocamlformat in docker images.Emilio Jesus Gallego Arias
2019-12-13Split up stdlib install command (too long)Gaëtan Gilbert
2019-12-13Merge PR #10657: restrict minimization to set to flexiblesMaxime Dénès
Reviewed-by: mattam82
2019-12-13Merge PR #11281: [vm] Untabify the VM C code.Maxime Dénès
Reviewed-by: maximedenes
2019-12-12Merge PR #11278: Clean libobject stuffGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
Split from #10331 Fix part of #8196 Replaces #9343
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
This is a follow up of #11010 ; I've realized that for example in #11123 a large part of the patch is detabification as indeed the files are mixed in tabs/space style so developers are forced to do the cleanup each time they work on them. Command used: ``` for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` Checked empty diff with `git diff --ignore-all-space`
2019-12-12Merge PR #11264: Type safe summary & libobject implementationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on ↵Emilio Jesus Gallego Arias
only-printing notations Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-12-11Remove the unused add_leaves Libobject primitive.Pierre-Marie Pédrot
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
This was just dead code.
2019-12-11Merge PR #11201: remove *.vos and *.vok file in "make clean"Enrico Tassi
Reviewed-by: gares
2019-12-11Merge PR #11262: [hashset] Don't use deprecated Obj.truncatePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ↵Pierre-Marie Pédrot
containing letins. Reviewed-by: ppedrot
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-10Merge PR #11269: Several cleanups and factorization in scheme declarationsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
Some calls are actually guarded by a check that the scheme is already in the cache. There is no reason to generate dummy side-effects in that case.
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-10Merge PR #11268: dune: Add byte mode for coqchk and coqide (fix dune-dbg for ↵Emilio Jesus Gallego Arias
dune 2) Reviewed-by: ejgallego
2019-12-09dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2)Gaëtan Gilbert
dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they now need explicit modes to be produced.
2019-12-09Type-safe implementation of libobjects.Pierre-Marie Pédrot
Same justification as the change in implementation of Summary.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:47:04 +0000