aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
* Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵Gravatar Maxime Dénès2017-10-20
|\ | | | | | | just Iris
| * rename ci-iris-coq -> ci-iris-lambda-rustGravatar Ralf Jung2017-10-19
| |
| * CI: build lambdaRust (which depends on Iris) rather than just IrisGravatar Ralf Jung2017-10-19
| |
* | Bugzilla autolink: avoid linking inside links (fix #5974).Gravatar Gaëtan Gilbert2017-10-18
|/
* Merge PR #540: [configure] Support for flambda flags.Gravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #1067: Iris CI: use opam to install dependenciesGravatar Maxime Dénès2017-10-10
|\ \
| | * [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-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 BugzillaGravatar Maxime Dénès2017-10-09
|\ \
* \ \ Merge PR #1117: [ci] Remove temporary bignums overlay.Gravatar Maxime Dénès2017-10-09
|\ \ \
* | | | Extract changes to the XML protocol from its docGravatar Théo Zimmermann2017-10-06
| | | |
* | | | Make the XML protocol doc more version-independentGravatar Théo Zimmermann2017-10-06
| | | |
* | | | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresGravatar Maxime Dénès2017-10-05
|\ \ \ \
| | * | | [ci] Remove temporary bignums overlay.Gravatar Théo Zimmermann2017-10-04
| |/ / / |/| | |
| | * | autolink to Github PRs from BugzillaGravatar Paul Steckler2017-10-03
| |/ / |/| |
* | | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Gravatar Maxime Dénès2017-10-03
|\ \ \
| | * | Fix GeoCoq build by using a shared CI configure.Gravatar Théo Zimmermann2017-10-03
| |/ / |/| | | | | | | | See also GeoCoq/GeoCoq#7.
* | | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileGravatar Maxime Dénès2017-10-03
|\ \ \
| | | * start counting at 0...Gravatar Ralf Jung2017-09-29
| | | |
| | | * Iris CI: use opam to determine std++ git commitGravatar Ralf Jung2017-09-29
| |_|/ |/| |
| | * Browser userscript to turn BZ#XXXX occurences into links.Gravatar Gaëtan Gilbert2017-09-27
| |/ |/|
* | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \
* \ \ Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ | | | | | | | | | | | | expected.
* | | | Do not reinstall preinstalled packages under AppVeyor.Gravatar Maxime Dénès2017-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.Gravatar Maxime Dénès2017-09-21
| | | |
| * | | In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gravatar Gaëtan Gilbert2017-09-20
|/ / /
| * | Improve documentation of Status message.Gravatar Maxime Dénès2017-09-19
| | |
* | | Merge PR #1043: Disable OSX signing for temporary artifacts.Gravatar Maxime Dénès2017-09-19
|\ \ \ | |/ / |/| |
* | | Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ | | | | | | | | | | | | | | | top of the linking chain.
* \ \ \ \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \
| | | * | | Fix GitLab CIGravatar Gaëtan Gilbert2017-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.Gravatar Maxime Dénès2017-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.Gravatar Théo Zimmermann2017-09-08
| |_|_|/ / |/| | | |
* | | | | Merge PR #968: Better error messages on the CIGravatar Maxime Dénès2017-09-07
|\ \ \ \ \
| | | | | * dev/build/windows/makecoq_mingw.sh: install camlp5's META fileGravatar Enrico Tassi2017-09-07
| | | | | |
* | | | | | Merge PR #914: Making the detyper lazyGravatar Maxime Dénès2017-09-07
|\ \ \ \ \ \
| | | | | | * Trying to properly propagate errors in Windows CI script.Gravatar Maxime Dénès2017-09-07
| |_|_|_|_|/ |/| | | | |
* | | | | | Make AppVeyor generate Windows package.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Remove -debug option from Windows build script.Gravatar Maxime Dénès2017-09-05
| | | | | | | | | | | | | | | | | | | | | | | | It is no longer accepted by Coq's ./configure.
* | | | | | Get sources of cygwin packages after building the installer.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Adapt Windows build script to new CoqIDE data installation directory.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Print more of the Coq build output.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Print Coq build output.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | In regression test mode, run cygwin setup to install dependencies.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Fix Software Foundations build.Gravatar Maxime Dénès2017-09-05
| |_|_|_|/ |/| | | | | | | | | | | | | | The Software Foundations archive has been replaced by three volumes.
| * | | | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-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.
* | | | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundGravatar Maxime Dénès2017-08-31
|\ \ \ \
| * | | | mention issue with OCAMLRUNPARAM and ocamldebugGravatar Paul Steckler2017-08-29
| | | | |
| | | | * [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
| | |_|/ | |/| | | | | | | | | | linking chain.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 08:37:23 +0000