aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-03Add .byte targets for every bestocaml targetGaëtan Gilbert
This makes it easier to compile our executables for debug purposes.
2018-05-03Merge PR #7400: ci-vst.sh: use -o progsEmilio Jesus Gallego Arias
2018-05-03Merge PR #7402: [ci]: add pidetop (fix #7336)Emilio Jesus Gallego Arias
2018-05-02[ci]: add pidetop (fix #7336)Enrico Tassi
2018-05-02Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`Théo Zimmermann
2018-05-02Merge PR #7403: Makefile doc ownersThéo Zimmermann
2018-05-02Fix Makefile.ci pattern in CODEOWNERSMaxime Dénès
2018-05-02Make doc owners also own Makefile.docMaxime Dénès
2018-05-02Merge PR #7394: [ci] [travis] Install num by default in all switches.Gaëtan Gilbert
2018-05-02Merge PR #7370: Fix PHONY typo in coq_makefileEnrico Tassi
2018-05-01Merge PR #7305: [toplevel] improve indentationEmilio Jesus Gallego Arias
2018-05-01ci-vst.sh: use -o progsGaëtan Gilbert
This is closer to what we mean than reproducing the default target without progs.
2018-05-01Merge PR #7397: [ci] Fix #7396: VST is brokenGaëtan Gilbert
2018-05-01[ci] Fix #7396: VST is brokenEmilio Jesus Gallego Arias
This is due to our CI script relying on their makefile internals, unfortunately we still have to do this to avoid timeouts.
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
`Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
2018-04-30[ci] [travis] Install num by default in all switches.Emilio Jesus Gallego Arias
This makes sense and simplifies the script a bit. In preparation for a more uniform, Docker-based base image.
2018-04-30Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives.Théo Zimmermann
2018-04-30Merge PR #6935: Separate universe minimization and evar normalization functionsPierre-Marie Pédrot
2018-04-30Merge PR #6944: Strict focusing using Default Goal Selector.Pierre-Marie Pédrot
2018-04-30Merge PR #7355: [owners] Makefile.ci belongs to the CI category.Maxime Dénès
2018-04-30Merge PR #6958: [lib] Move global options to their proper place.Maxime Dénès
2018-04-30[doc] Update Sphinx build instructions for Debian derivatives.Emilio Jesus Gallego Arias
We update the instructions a bit providing the name of the Debian packages, we also mention Nix and add to .gitignore a Sphinx-autogenerated file.
2018-04-30Merge PR #7381: [gitlab] Update base image to Ubuntu bionic + some improvements.Gaëtan Gilbert
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
2018-04-29tclSELECT: SelectAll never happensGaëtan Gilbert
2018-04-29[gitlab] Update base image to Ubuntu bionic + some improvements.Emilio Jesus Gallego Arias
We move gitlab runners to Ubuntu 18.04 "Bionic"; this allows us to install most base dependencies using APT, and opens up the door to saving quite a bit of time by creating a custom docker image [c.f. #7383] This change comes with an update of dependencies; we tweak them. Also: - we add a more precise cache `key` constraint; this is still done manually, we should develop an automated way in another PR. The format is "$image-v$date-$hour-$minute" - we export DEBIAN_FRONTEND=noninteractive as to avoid problems with package installs that ask for interactive input. - we install Sphinx Python packages using `apt` save for python3-antlr4, which is still unpackaged [see https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=897129]
2018-04-29Merge PR #7386: [doc] Remove unused dependencies.Théo Zimmermann
2018-04-28[doc] Remove unused dependencies.Emilio Jesus Gallego Arias
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
2018-04-28Merge PR #7376: Fix gitlab ubuntu versionEmilio Jesus Gallego Arias
2018-04-28Fix gitlab ubuntu versionGaëtan Gilbert
Newer versions don't have the latex packages we want. see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131
2018-04-28Merge PR #7357: [CI] elpi 1.0 has an official opam packageEmilio Jesus Gallego Arias
2018-04-28Merge PR #7367: circle CI: do not use cache from old config.yml versionsEmilio Jesus Gallego Arias
2018-04-28Merge PR #6892: Cleanup implementation of normalize_context_set a bitPierre-Marie Pédrot
2018-04-27Fix PHONY typo in coq_makefileGaëtan Gilbert
2018-04-27[CI] elpi 1.0 has an official opam packageEnrico Tassi
2018-04-27circle CI: do not use cache from old config.yml versionsGaëtan Gilbert
It begs things to break when the cache is out of sync with the system packages.
2018-04-27Merge PR #7358: Fix #7356: missing lift when interpreting default instances ↵Enrico Tassi
of evars
2018-04-27Merge PR #7351: Always print explanation for univ inconsistency, rm ↵Emilio Jesus Gallego Arias
Flags.univ_print
2018-04-26Merge PR #7321: configure: make -annotate fatal, and color error and warningsEmilio Jesus Gallego Arias
2018-04-26Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)Emilio Jesus Gallego Arias
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-26[owners] Makefile.ci belongs to the CI category.Emilio Jesus Gallego Arias
2018-04-26Merge PR #7331: Fix a typo in the reference manual: <; -> <:Maxime Dénès
2018-04-26Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bitMaxime Dénès
2018-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
2018-04-25updating CI for Mtac2Beta Ziliani
2018-04-25Merge PR #7290: Update debugging.mdHugo Herbelin
2018-04-25Merge PR #6866: Slight improvement of messages related to direct and ↵Pierre-Marie Pédrot
indirect uses of tactic `clear`.
2018-04-25Merge PR #7322: Test suite Makefile: print message for failing tests as they ↵Enrico Tassi
come, misc improvements
2018-04-24Merge PR #307: Adding a flag to support different naming modes for evar ↵Pierre-Marie Pédrot
hypotheses.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:47:23 +0000