Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update configure.ml to only warn on lablgtk 2.16.0 | 2018-01-16 | |
| | | | | | | | | | | | The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0 even for much newer versions. This makes building Coq on Ubuntu impossible without modifying configure. This commit fixes that problem. See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for the upstream bug. This closes #6585 | ||
* | Merge PR #6578: Remove references to deleted Unicode.Unsupported exception | 2018-01-13 | |
|\ | |||
* \ | Merge PR #6581: Added newline at the end of usage of coqdep. | 2018-01-13 | |
|\ \ | |||
* \ \ | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 2018-01-13 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6483: Strong invariants in polymorphic definitions | 2018-01-12 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6288: Interfaces for checker and IDE. | 2018-01-12 | |
|\ \ \ \ \ | |||
| | * | | | | Adding a custom Travis overlay for HoTT. | 2018-01-11 | |
| | | | | | | |||
| | * | | | | Enforce that polymorphic definitions do not generate internal constraints. | 2018-01-11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In practice, we only send to the kernel polymorphic definitions whose side-effects have been exported first, and furthermore their bodies have already been forced. Therefore, no constraints are generated by the kernel. Nonetheless, it might be desirable in the future to also defer computation of polymorphic proofs whose constraints have been explicited in the type. It is not clear when this is going to be implemented. Nonetheless, the current check is not too drastic as it only prevents monomorphic side-effects to appear inside polymorphic opaque definitions. The only way I know of to trigger such a situation is to generate a scheme in a proof, as even abstract is actually preserving the polymorphism status of the surrounding proof. It would be possible to work around such rare instances anyways. As for internal constraints generated by a potentially deferred polymorphic body, it is easy to check that they are a subset of the exported ones at a higher level inside the future computation and fail there. So in practice this patch is not too restrictive and it highlights a rather strong invariant of the kernel code. | ||
| | | * | | | Document test-suite PRINT_LOGS. | 2018-01-11 | |
| | | | | | | |||
| | | * | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 2018-01-11 | |
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1 | ||
* | | | | | Merge PR #6557: First stab at documenting the test suite. | 2018-01-11 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6552: [PR template] Remove the relative link to CHANGES. | 2018-01-11 | |
|\ \ \ \ \ \ | |||
| | | | | * | | Added newline at the end of usage of coqdep. | 2018-01-11 | |
| |_|_|_|/ / |/| | | | | | |||
| | | | * | | Force polymorphic definitions to have no internal constraints. | 2018-01-11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else. | ||
| | | | | * | Remove references to removed Unicode.Unsupported | 2018-01-11 | |
| |_|_|_|/ |/| | | | | | | | | | | | | | | This exception was removed in [on Oct 13, 2016](https://github.com/coq/coq/commit/57c6ffd23836364168ffd1c66dbddbecf830c7c6#diff-297bc4c11289c2c0ed18d5eebf817c47). | ||
| | * | | | Lint and remove redundant line | 2018-01-11 | |
| | | | | | |||
| | | * | | Add interfaces for IDE and remove dead code. | 2018-01-10 | |
| | | | | | | | | | | | | | | | | | | | | Should fix #6177, which was triggered by lonely .ml files. | ||
| | | * | | Add interfaces for checker and remove dead code. | 2018-01-10 | |
| |_|/ / |/| | | | |||
* | | | | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label | 2018-01-10 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6570: [meta] Fix typo on Coq's META file following #6444. | 2018-01-10 | |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| | | | * | Add comments by @psteckler to test-suite/README.md | 2018-01-10 | |
| | | | | | |||
| * | | | | [meta] Fix typo on Coq's META file following #6444. | 2018-01-09 | |
|/ / / / | |||
* | | | | Merge PR #6532: Fix mli-doc issue #6531 | 2018-01-08 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6489: Update PNGs; mention async error handling; change query ↵ | 2018-01-08 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | window to query pane in text | ||
* \ \ \ \ \ | Merge PR #6497: Add optimize_heap tactic for #6488 | 2018-01-08 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6549: Normalize package names | 2018-01-08 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6533: Update the lower-bound of the lablgtk dependency. | 2018-01-08 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6425: Cleanup universes in the kernel | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6530: Ignore generated test-suite/output/MExtraction.out | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6517: Trim more trailing whitespace in coq-makefile timing test | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6527: Update backport script for more control. | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6526: Fixing various typos in the Credits chapter. | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | * | | | github-check-prs.py: print PR URLs when needed. | 2018-01-08 | |
| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | * | | | github-check-prs.py: Strip spaces from token from command line | 2018-01-08 | |
| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | * | | | github-check-prs.py: command line option to get token from a file | 2018-01-08 | |
| | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | Merge PR #6510: Document between and exists_between types. | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | | | | | | Document between and exists_between types. | 2018-01-08 | |
| | | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | | Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06 | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6501: Document use of ocamldebug from the command line in ↵ | 2018-01-08 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cygwin/Windows | ||
| | | | | | | | | | | | | | | | | * | Mention -B argument of make to rerun tests | 2018-01-07 | |
| | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | First stab at documenting the test suite. | 2018-01-06 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | * | [PR template] Remove the relative link. | 2018-01-05 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was actually pointing to https://github.com/CHANGES. | ||
| | | | | | | | | | | * | | | | | Normalize MacOS installer name. | 2018-01-04 | |
| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | Normalize Windows installer names. | 2018-01-04 | |
| |_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | |||
| | | | | | | | | | * | | | | | Update the lower-bound of the lablgtk dependency. | 2018-01-04 | |
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Closes #6509. | ||
| | | | | | | | | | * | | | | add optimize_heap tactic for #6488 | 2018-01-03 | |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | update PNGs; mention async error handling; change query window to query ↵ | 2018-01-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | pane; use color descriptions | ||
| | | | | | | | | | | | * | | Fix mli-doc issue #6531 | 2018-01-01 | |
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |||
| | | | | | | * | | | | | | Ignore generated test-suite/output/MExtraction.out | 2017-12-31 | |
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | |