aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-10Merge PR #540: [configure] Support for flambda flags.Maxime Dénès
2017-10-10Merge PR #1067: Iris CI: use opam to install dependenciesMaxime Dénès
2017-10-10[configure] Support for flambda flags.Emilio Jesus Gallego Arias
We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
2017-10-09Merge PR #1115: Autolink to Github PRs from BugzillaMaxime Dénès
2017-10-09Merge PR #1117: [ci] Remove temporary bignums overlay.Maxime Dénès
2017-10-06Extract changes to the XML protocol from its docThéo Zimmermann
2017-10-06Make the XML protocol doc more version-independentThéo Zimmermann
2017-10-05Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresMaxime Dénès
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
2017-10-03autolink to Github PRs from BugzillaPaul Steckler
2017-10-03Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Maxime Dénès
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
See also GeoCoq/GeoCoq#7.
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-09-29start counting at 0...Ralf Jung
2017-09-29Iris CI: use opam to determine std++ git commitRalf Jung
2017-09-27Browser userscript to turn BZ#XXXX occurences into links.Gaëtan Gilbert
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Maxime Dénès
expected.
2017-09-21Do not reinstall preinstalled packages under AppVeyor.Maxime Dénès
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.
2017-09-21Print Cygwin setup output rather than logging in to a file.Maxime Dénès
2017-09-20In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gaëtan Gilbert
2017-09-19Improve documentation of Status message.Maxime Dénès
2017-09-19Merge PR #1043: Disable OSX signing for temporary artifacts.Maxime Dénès
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Maxime Dénès
top of the linking chain.
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-09-13Fix GitLab CIGaëtan Gilbert
- 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.
2017-09-11Disable OSX signing for temporary artifacts.Maxime Dénès
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.
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07dev/build/windows/makecoq_mingw.sh: install camlp5's META fileEnrico Tassi
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Trying to properly propagate errors in Windows CI script.Maxime Dénès
2017-09-05Make AppVeyor generate Windows package.Maxime Dénès
2017-09-05Remove -debug option from Windows build script.Maxime Dénès
It is no longer accepted by Coq's ./configure.
2017-09-05Get sources of cygwin packages after building the installer.Maxime Dénès
2017-09-05Adapt Windows build script to new CoqIDE data installation directory.Maxime Dénès
2017-09-05Print more of the Coq build output.Maxime Dénès
2017-09-05Print Coq build output.Maxime Dénès
2017-09-05In regression test mode, run cygwin setup to install dependencies.Maxime Dénès
2017-09-05Fix Software Foundations build.Maxime Dénès
The Software Foundations archive has been replaced by three volumes.
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
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.
2017-08-31Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundMaxime Dénès
2017-08-29mention issue with OCAMLRUNPARAM and ocamldebugPaul Steckler
2017-08-29[general] Merge parsing with highparsing, put toplevel at the top of the ↵Emilio Jesus Gallego Arias
linking chain.
2017-08-29Adapt debugging doc to configure/Makefile changes.Théo Zimmermann
2017-08-29Move debugging to Markdown.Théo Zimmermann
With a minimal diff (so I'm not putting quotes ` ` around all the code).
2017-08-29Move dev/doc/changes to Markdown.Théo Zimmermann
And remove old French part. And move part about the plugin API to the right section.
2017-08-29Merge PR #838: Have coq-dpdgraph ci test print the differencesMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:38:38 +0000