Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | Add linter. | 2017-10-25 | ||
| | | | ||||
* | | | Merge PR #6003: Point HoTT back at master, which now supports Coq master | 2017-10-25 | ||
|\ \ \ | ||||
| * | | | Point HoTT back at master, which now supports Coq master | 2017-10-23 | ||
| | | | | ||||
* | | | | Switch testing branch back to CompCert upstream. | 2017-10-20 | ||
| |/ / |/| | | | | | | | | This follows the merge of AbsInt/CompCert#191. | |||
* | | | Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵ | 2017-10-20 | ||
|\ \ \ | | | | | | | | | | | | | just Iris | |||
| * | | | rename ci-iris-coq -> ci-iris-lambda-rust | 2017-10-19 | ||
| | | | | ||||
| * | | | CI: build lambdaRust (which depends on Iris) rather than just Iris | 2017-10-19 | ||
| |/ / | ||||
* / / | Bugzilla autolink: avoid linking inside links (fix #5974). | 2017-10-18 | ||
|/ / | ||||
* | | Merge PR #540: [configure] Support for flambda flags. | 2017-10-10 | ||
|\ \ | ||||
* \ \ | Merge PR #1067: Iris CI: use opam to install dependencies | 2017-10-10 | ||
|\ \ \ | ||||
| | * | | [configure] Support for flambda flags. | 2017-10-10 | ||
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ``` | |||
* | | | Merge PR #1115: Autolink to Github PRs from Bugzilla | 2017-10-09 | ||
|\ \ \ | ||||
* \ \ \ | Merge PR #1117: [ci] Remove temporary bignums overlay. | 2017-10-09 | ||
|\ \ \ \ | |_|_|/ |/| | | | ||||
* | | | | Extract changes to the XML protocol from its doc | 2017-10-06 | ||
| | | | | ||||
* | | | | Make the XML protocol doc more version-independent | 2017-10-06 | ||
| | | | | ||||
* | | | | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | 2017-10-05 | ||
|\ \ \ \ | ||||
| | * | | | [ci] Remove temporary bignums overlay. | 2017-10-04 | ||
| |/ / / |/| | | | ||||
| | * | | autolink to Github PRs from Bugzilla | 2017-10-03 | ||
| |/ / |/| | | ||||
* | | | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links. | 2017-10-03 | ||
|\ \ \ | ||||
| | * | | Fix GeoCoq build by using a shared CI configure. | 2017-10-03 | ||
| |/ / |/| | | | | | | | | See also GeoCoq/GeoCoq#7. | |||
* | | | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file | 2017-10-03 | ||
|\ \ \ | ||||
| | | * | start counting at 0... | 2017-09-29 | ||
| | | | | ||||
| | | * | Iris CI: use opam to determine std++ git commit | 2017-09-29 | ||
| |_|/ |/| | | ||||
| | * | Browser userscript to turn BZ#XXXX occurences into links. | 2017-09-27 | ||
| |/ |/| | ||||
* | | Merge PR #1055: Remove STM vernaculars | 2017-09-22 | ||
|\ \ | ||||
* \ \ | Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵ | 2017-09-22 | ||
|\ \ \ | | | | | | | | | | | | | expected. | |||
* | | | | Do not reinstall preinstalled packages under AppVeyor. | 2017-09-21 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it. | |||
* | | | | Print Cygwin setup output rather than logging in to a file. | 2017-09-21 | ||
| | | | | ||||
| * | | | In gitlab set TRAVIS_BRANCH so user overlays will work as expected. | 2017-09-20 | ||
|/ / / | ||||
| * | | Improve documentation of Status message. | 2017-09-19 | ||
| | | | ||||
* | | | Merge PR #1043: Disable OSX signing for temporary artifacts. | 2017-09-19 | ||
|\ \ \ | |/ / |/| | | ||||
* | | | Merge PR #979: Fix install-doc target and other gitlab failures | 2017-09-15 | ||
|\ \ \ | ||||
* \ \ \ | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵ | 2017-09-15 | ||
|\ \ \ \ | | | | | | | | | | | | | | | | top of the linking chain. | |||
* \ \ \ \ | Merge PR #962: Move dev/doc/changes to Markdown. | 2017-09-15 | ||
|\ \ \ \ \ | ||||
| | | * | | | Fix GitLab CI | 2017-09-13 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - timing needs time and python - check for compiled files without source looks in the install directory (except for make -f Makefile.ci which doesn't check), as such the install directory has been renamed to _install_ci and isn't searched. | |||
| | | | * | | Disable OSX signing for temporary artifacts. | 2017-09-11 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The OSX binaries were signed twice with a fake identity, leading to some obscure errors on Travis in some cases. We disable code signing for Travis artifacts. For released packages, a proper signing will be applied manually. | |||
* | | | | | | Move README.ci and link to it from CONTRIBUTING. | 2017-09-08 | ||
| |_|_|/ / |/| | | | | ||||
* | | | | | Merge PR #968: Better error messages on the CI | 2017-09-07 | ||
|\ \ \ \ \ | ||||
| | | | | * | dev/build/windows/makecoq_mingw.sh: install camlp5's META file | 2017-09-07 | ||
| | | | | | | ||||
* | | | | | | Merge PR #914: Making the detyper lazy | 2017-09-07 | ||
|\ \ \ \ \ \ | ||||
| | | | | | * | Trying to properly propagate errors in Windows CI script. | 2017-09-07 | ||
| |_|_|_|_|/ |/| | | | | | ||||
* | | | | | | Make AppVeyor generate Windows package. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | Remove -debug option from Windows build script. | 2017-09-05 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | It is no longer accepted by Coq's ./configure. | |||
* | | | | | | Get sources of cygwin packages after building the installer. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | Adapt Windows build script to new CoqIDE data installation directory. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | Print more of the Coq build output. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | Print Coq build output. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | In regression test mode, run cygwin setup to install dependencies. | 2017-09-05 | ||
| | | | | | | ||||
* | | | | | | Fix Software Foundations build. | 2017-09-05 | ||
| |_|_|_|/ |/| | | | | | | | | | | | | | | The Software Foundations archive has been replaced by three volumes. | |||
| * | | | | Making detyping potentially lazy. | 2017-09-04 | ||
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. |