aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-09-13Reference manual: A few words about the file system constraints for -Q/-R.Hugo Herbelin
2017-09-13Adding a test for utf8 characters in directory names.Hugo Herbelin
2017-09-13A possible fix for BZ#5715 (escape non-utf8 win32 file names).Hugo Herbelin
On Win32, Sys.readdir translates the file names to the charset of the local "code page", which may be not compatible with utf8. Warnings referring to these names can be generated. These warnings may be sent to CoqIDE. To ensure a utf8 compliant communication, we escape non-utf8 file names under win32. In the CoqIDE/Coq communication, Glib.IO.read_chars expects an utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in conversion input". This fixes bug #5715 (Hangul characters not recognized in file names) but this does not solve the case of an operating system mounting a file system with a different coding convention than the default one, i.e. unicode using "Normalization Form Canonical Decomposition" in UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux, (non-normalized?) UTF-16 for NTFS on Windows.
2017-09-13Complying more precisely to unicode standard.Hugo Herbelin
In particular, checking that it is at most 4 bytes.
2017-09-13Adding a function to escape strings with non-utf8 characters.Hugo Herbelin
2017-09-13Supporting library names in utf8 in coqdep.Hugo Herbelin
2017-09-12Removing now useless former fix to #3333 (check valid module names).Hugo Herbelin
The fix is not anymore needed after Id.of_string was made strict (5b218f87). This allows to support the whole official syntax of identifiers and not just the alpha-numerical ones (without quote).
2017-09-11Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right ↵Maxime Dénès
artificially restricted to a non-empty context).
2017-09-11Merge PR #1032: Make our CI policy clearer and more explicitMaxime Dénès
2017-09-11Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Maxime Dénès
2017-09-11Merge PR #1035: Fix the introduction of SSR refman chapter.Maxime Dénès
2017-09-11Merge PR #1029: Fix a refine anomaly "Evar defined twice".Maxime Dénès
2017-09-11Merge PR #1014: Add option index entry for NativeCompute ProfilingMaxime Dénès
2017-09-11Merge PR #1004: Document primitive projections in more detailMaxime Dénès
2017-09-11Merge PR #987: In Array.smartmap, read and write from same arrayMaxime Dénès
2017-09-08Fix Typo in Doc for `Set Parsing Explicit`staffehn
2017-09-08Fix the introduction of SSR refman chapter.Théo Zimmermann
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-08Update CI policy.Théo Zimmermann
2017-09-07Merge PR #997: coqdoc: Support comments in verbatim outputMaxime Dénès
2017-09-07Merge PR #1016: 2 Typos in 'Add Parametric Morphism' DocumentationMaxime Dénès
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07Merge PR #931: Parametrize module bodyMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Merge PR #904: Add build_coq_or to API.CoqlibMaxime Dénès
2017-09-06Fix a refine anomaly "Evar defined twice".Pierre-Marie Pédrot
Because the argument given to refine may mess with the evarmap, the goal being refined can be solved by side-effect after the term filler is computed. If this happens, we simply don't perform the refining operation.
2017-09-06Merge PR #1022: Appveyor packageMaxime 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-05Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ↵Maxime Dénès
#958
2017-09-05Merge PR #1020: .mailmap updateGuillaume Melquiond
2017-09-05Merge PR #1010: Move mention of native_compute profiling in CHANGESMaxime Dénès
2017-09-05Merge PR #1021: Fix Software Foundations build.Maxime Dénès
2017-09-05.mailmap updateGaëtan Gilbert
2017-09-05Fix Software Foundations build.Maxime Dénès
The Software Foundations archive has been replaced by three volumes.
2017-09-04fix test-suite/coq-makefile/findlib-package on windowsEnrico Tassi
2017-09-04Merge PR #1018: Avoid reinstalling some Cygwin dependencies on AppVeyor.Maxime Dénès
2017-09-04Avoid reinstalling some Cygwin dependencies on AppVeyor.Maxime Dénès
For some reason, OPAM was not happy after we reinstalled curl.
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-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it.
2017-09-032 Typos in 'Add Parametric Morphism' Documentationstaffehn
2017-09-01add option index entry for NativeCompute ProfilingPaul Steckler
2017-09-01move mention of native_compute profiling in CHANGESPaul Steckler
2017-09-01Bump MacOS version number and magic numbers.Maxime Dénès
2017-09-01Change version string to 8.8+alpha.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:56:00 +0000