Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | * | | | | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | 2018-02-07 | |
| |_|/ / / / |/| | | | | | ||||
* | | | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | Maxime Dénès | 2018-02-06 | |
|\ \ \ \ \ \ | ||||
| | | * | | | | Points to Flocq official repository. | Théo Zimmermann | 2018-02-05 | |
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| | * | | | | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | 2018-02-05 | |
| | | | | | | ||||
* | | | | | | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | 2018-02-05 | |
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | | ||||
| | * | | | | [stm] [toplevel] Make loadpath a parameter of the document. | Emilio Jesus Gallego Arias | 2018-02-05 | |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc... | |||
| * | | | | CI: Run coqchk on Iris | Ralf Jung | 2018-01-31 | |
| | |_|/ | |/| | | ||||
* | | | | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵ | Maxime Dénès | 2018-01-31 | |
|\ \ \ \ | | | | | | | | | | | | | | | | menhir. | |||
* \ \ \ \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 | |
|\ \ \ \ \ | ||||
| | * | | | | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | 2018-01-30 | |
| | |/ / / | ||||
| * | | | | Adding an overlay for Equations. | Pierre-Marie Pédrot | 2018-01-30 | |
| | | | | | ||||
* | | | | | Merge PR #6605: Safer VM interfaces | Maxime Dénès | 2018-01-30 | |
|\ \ \ \ \ | ||||
| * | | | | | Safer VM interfaces | Maxime Dénès | 2018-01-26 | |
| | |/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays. | |||
* / | | | | Use travis_retry on apt-get update | Jason Gross | 2018-01-23 | |
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration. | |||
* | | | | Merge PR #6629: Archive COMPATIBILITY | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #6568: Cleanup scripts | Maxime Dénès | 2018-01-23 | |
|\ \ \ \ \ | ||||
| | * | | | | Archive COMPATIBILITY. | Théo Zimmermann | 2018-01-22 | |
| | | | | | | ||||
* | | | | | | Merge PR #6550: Remove outdated note about rlwrap in setup.txt | Maxime Dénès | 2018-01-22 | |
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | | ||||
* | | | | | | Merge PR #6448: Cleanup and add debug printers a bit | Maxime Dénès | 2018-01-18 | |
|\ \ \ \ \ \ | ||||
| | | * | | | | merge-pr.sh: use git diff --quiet | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | ||||
| | | * | | | | Source basic overlay before user overlays. | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | ||||
| | | * | | | | Cleanup shell expansions and quoting. | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | ||||
| | | * | | | | Simplify logic and streamline lint-repository.sh | Gaëtan Gilbert | 2018-01-16 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation. | |||
* | | | | | | | Fix the wrapper around ocamldebug. | Pierre-Marie Pédrot | 2018-01-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug | |||
* | | | | | | | Merge PR #6483: Strong invariants in polymorphic definitions | Maxime Dénès | 2018-01-12 | |
|\ \ \ \ \ \ \ | ||||
| * | | | | | | | Adding a custom Travis overlay for HoTT. | Pierre-Marie Pédrot | 2018-01-11 | |
| | | | | | | | | ||||
* | | | | | | | | Merge PR #6557: First stab at documenting the test suite. | Maxime Dénès | 2018-01-11 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label | Maxime Dénès | 2018-01-10 | |
|\ \ \ \ \ \ \ \ \ | |_|/ / / / / / / |/| | | | | | | | | ||||
| | | | | | | * | | [Backport script] Check .mli files are not changed. | Théo Zimmermann | 2018-01-09 | |
| |_|_|_|_|_|/ / |/| | | | | | | | ||||
| | | | | * | | | Cleanup conditional in lint-repository.sh | Gaëtan Gilbert | 2018-01-08 | |
| | | | | |/ / | ||||
| | | | * / / | Stop talking about debian in "A note about rlwrap" | Gaëtan Gilbert | 2018-01-08 | |
| | | | |/ / | | | | | | | | | | | | | | | | | | | Debian stable version is 0.42-3 right now. | |||
* | | | | | | Merge PR #6549: Normalize package names | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #6527: Update backport script for more control. | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ | ||||
| | | * | | | | | github-check-prs.py: print PR URLs when needed. | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | ||||
| | | * | | | | | github-check-prs.py: Strip spaces from token from command line | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | ||||
| | | * | | | | | github-check-prs.py: command line option to get token from a file | Gaëtan Gilbert | 2018-01-08 | |
| | | | | | | | | ||||
* | | | | | | | | Merge PR #6501: Document use of ocamldebug from the command line in ↵ | Maxime Dénès | 2018-01-08 | |
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | Cygwin/Windows | |||
| | | | | * | | | First stab at documenting the test suite. | Jasper Hugunin | 2018-01-06 | |
| |_|_|_|/ / / |/| | | | | | | ||||
| | | | | | * | Remove dir-locals and ship suggested helper hooks instead. | Gaëtan Gilbert | 2018-01-06 | |
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | .dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings. | |||
| | | * | | | Normalize MacOS installer name. | Théo Zimmermann | 2018-01-04 | |
| | | | | | | ||||
| | | * | | | Normalize Windows installer names. | Théo Zimmermann | 2018-01-04 | |
| |_|/ / / |/| | | | | ||||
| | | * | | Expound on dependencies for github-check-prs.py | Gaëtan Gilbert | 2017-12-30 | |
| | | | | | ||||
| | | * | | Python script checking missing/unnecessary [needs: rebase] label | Gaëtan Gilbert | 2017-12-30 | |
| | | | | | ||||
| * | | | | Add instructions for debugging from the command line (and in Windows) | Jim Fehrle | 2017-12-29 | |
| | | | | | | | | | | | | | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows) | |||
* | | | | | Merge PR #6493: [API] remove large file containing duplicate interfaces | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #6405: Remove the local polymorphic flag hack. | Maxime Dénès | 2017-12-29 | |
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | | | ||||
| | * | | | | overlay for #6493 | Enrico Tassi | 2017-12-27 | |
| | | | | | | ||||
| | * | | | | [API] remove large file containing duplicate interfaces | Enrico Tassi | 2017-12-27 | |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | |||
* | | | | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failing | Maxime Dénès | 2017-12-27 | |
|\ \ \ \ \ | ||||
| | * | | | | Add equations overlay. | Maxime Dénès | 2017-12-27 | |
| |/ / / / |/| | | | |