| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-02 | [ci]: add pidetop (fix #7336) | Enrico Tassi | |
| 2018-05-02 | Fix #7214: install knows which ml files do not get compiled to cmx. | Gaëtan Gilbert | |
| 2018-05-02 | Remove unused Deque files | Gaëtan Gilbert | |
| 2018-05-02 | Merge PR #7339: [api] Move bullets and goals selectors to `proofs/` | Théo Zimmermann | |
| 2018-05-02 | Merge PR #7403: Makefile doc owners | Théo Zimmermann | |
| 2018-05-02 | first examples of commands taking arguments | Yves Bertot | |
| 2018-05-02 | Fix Makefile.ci pattern in CODEOWNERS | Maxime Dénès | |
| 2018-05-02 | Make doc owners also own Makefile.doc | Maxime Dénès | |
| 2018-05-02 | Merge PR #7394: [ci] [travis] Install num by default in all switches. | Gaëtan Gilbert | |
| 2018-05-02 | Merge PR #7370: Fix PHONY typo in coq_makefile | Enrico Tassi | |
| 2018-05-01 | add usage explanations | Yves Bertot | |
| 2018-05-01 | Merge PR #7305: [toplevel] improve indentation | Emilio Jesus Gallego Arias | |
| 2018-05-01 | add a simple explanation in the README file | Yves Bertot | |
| 2018-05-01 | a first project on how to organize files and define a simple query | Yves Bertot | |
| 2018-05-01 | Automatically run alienclean before compiling. | Gaëtan Gilbert | |
| This removes the "leftover files without known source" error in favor of automatic handling. | |||
| 2018-05-01 | Actually take advantage of the normalization status of kernel closures. | Pierre-Marie Pédrot | |
| We know that when a fterm is marked as Whnf or Norm, the only thing that can happen in the reduction machine is administrative reduction pushing the destructured term on the stack. Thus there is no need to perform any actual performative reduction. Furthermore, every head subterm of those terms are recursively Whnf or Norm, which implies that no update mark is pushed on the stack during the destructuration. So there is no need to unzip the stack to unset FLOCKED nodes as well. | |||
| 2018-05-01 | ci-vst.sh: use -o progs | Gaëtan Gilbert | |
| This is closer to what we mean than reproducing the default target without progs. | |||
| 2018-05-01 | Merge PR #7397: [ci] Fix #7396: VST is broken | Gaëtan Gilbert | |
| 2018-05-01 | [ci] Fix #7396: VST is broken | Emilio 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-30 | Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives. | Théo Zimmermann | |
| 2018-04-30 | Merge PR #6935: Separate universe minimization and evar normalization functions | Pierre-Marie Pédrot | |
| 2018-04-30 | Adapt the VM GC hook to handle the no-naked-pointers option flag. | Pierre-Marie Pédrot | |
| The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers to C-allocated strings standing for VM bytecode. If the the no-naked-pointers option is set, we perform the check that a stack value lives on the OCaml heap ourselves. | |||
| 2018-04-30 | Make the VM accumulator look like an OCaml block. | Pierre-Marie Pédrot | |
| We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0. | |||
| 2018-04-30 | Wrap VM bytecode used on the OCaml side in an OCaml block. | Pierre-Marie Pédrot | |
| This prevents the existence of a few naked pointers to C heap from the OCaml heap. VM bytecode is represented as any block of size at least 1 whose first field points to a C-allocated string. This representation is compatible with the Coq VM representation of (potentially recursive) closures, which are already specifically tailored in the OCaml GC to be able to contain out-of-heap data. | |||
| 2018-04-30 | Merge PR #6944: Strict focusing using Default Goal Selector. | Pierre-Marie Pédrot | |
| 2018-04-30 | Merge PR #7355: [owners] Makefile.ci belongs to the CI category. | Maxime Dénès | |
| 2018-04-30 | Merge 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-30 | Merge PR #7381: [gitlab] Update base image to Ubuntu bionic + some improvements. | Gaëtan Gilbert | |
| 2018-04-29 | Strict 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-29 | tclSELECT: SelectAll never happens | Gaë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-29 | Fix the secondary maintainer for Makefile. | Théo Zimmermann | |
| Closes #7345. [skip ci] | |||
| 2018-04-29 | Change maintainers for universe files in the kernel / engine. | Théo Zimmermann | |
| Mitigates #7346. [skip ci] | |||
| 2018-04-29 | Implement to_constr with nf_evars_and_universes_opt_subst | Gaëtan Gilbert | |
| 2018-04-29 | Merge 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-28 | Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evars | Gaëtan Gilbert | |
| 2018-04-28 | Merge PR #7376: Fix gitlab ubuntu version | Emilio Jesus Gallego Arias | |
| 2018-04-28 | Fix gitlab ubuntu version | Gaëtan Gilbert | |
| Newer versions don't have the latex packages we want. see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131 | |||
| 2018-04-28 | Merge PR #7357: [CI] elpi 1.0 has an official opam package | Emilio Jesus Gallego Arias | |
| 2018-04-28 | Merge PR #7367: circle CI: do not use cache from old config.yml versions | Emilio Jesus Gallego Arias | |
| 2018-04-28 | Merge PR #6892: Cleanup implementation of normalize_context_set a bit | Pierre-Marie Pédrot | |
| 2018-04-27 | Fix PHONY typo in coq_makefile | Gaëtan Gilbert | |
| 2018-04-27 | [CI] elpi 1.0 has an official opam package | Enrico Tassi | |
| 2018-04-27 | circle CI: do not use cache from old config.yml versions | Gaëtan Gilbert | |
| It begs things to break when the cache is out of sync with the system packages. | |||
| 2018-04-27 | Merge PR #7358: Fix #7356: missing lift when interpreting default instances ↵ | Enrico Tassi | |
| of evars | |||
| 2018-04-27 | Merge PR #7351: Always print explanation for univ inconsistency, rm ↵ | Emilio Jesus Gallego Arias | |
| Flags.univ_print | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |