aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
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
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-24Don't strip the newline, don't use \rJason Gross
Not sure entirely what it was supposed to do, but stripping the newline erased the following line
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
Now the folded line starts with "Aggregating..." and not with "---------"
2017-08-24Only display travis_fold: on travisJason Gross
2017-08-18Merge PR #801: Make Travis generate OSX packages.Maxime Dénès
2017-08-17Make Travis generate OSX packages.Maxime Dénès
The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
2017-08-16Mention tclINDEPENDENTL (#349) in dev/doc/changes.Théo Zimmermann
2017-08-15Move the rest of the ci target to a bash fileJason Gross
2017-08-15Better error messages on the CIJason Gross
This makes it so that when a ci target fails, we don't get red herring error messages about .ok files not existing. Since this requires bash, we make a helper script that invokes bash, so as to not depend on bash in general.
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Remove obsolete filesGaëtan Gilbert
db_printers just isn't used. api.txt is superseded by the API OCaml interface.
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
This gives syntax highlighting in Coq-aware editors.
2017-08-01Remove dev/TODOGaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
They seem unused since 8f4b7f1 (2007).
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
This allows better debugging when it fails.
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-28Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:43:00 +0000