aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* A possible fix for BZ#5715 (escape non-utf8 win32 file names).Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | 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.
* Complying more precisely to unicode standard.Gravatar Hugo Herbelin2017-09-13
| | | | In particular, checking that it is at most 4 bytes.
* Adding a function to escape strings with non-utf8 characters.Gravatar Hugo Herbelin2017-09-13
|
* Merge PR #987: In Array.smartmap, read and write from same arrayGravatar Maxime Dénès2017-09-11
|\
* | 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 #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \
* \ \ Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵Gravatar Maxime Dénès2017-08-31
|\ \ \ | | | | | | | | | | | | implementation from Detyping.
* \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \
| | | * | Canonically renaming fold_map into fold_left_map in library Option.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | Also adding fold_right_map by consistency.
| | | * | Canonically renaming fold_map into fold_left_map in library Array.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | Also renaming fold_map' into fold_right_map, and fold_map2' into fold_right2_map.
| | | * | Adding combinators + a canonical renaming in cList.ml.Gravatar Hugo Herbelin2017-08-29
| |_|/ / |/| | | | | | | | | | | | | | | - Adding fold_left2_map/fold_right2_map. - Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
| | | * also in Fun1.smartmap, read, write from same arrayGravatar Paul Steckler2017-08-22
| | | |
| | * | Prevent overallocation in Array.map_to_list and remove custom implementation ↵Gravatar Guillaume Melquiond2017-08-22
| |/ / |/| | | | | | | | from Detyping.
| | * read, write from same arrayGravatar Paul Steckler2017-08-21
| |/ |/|
* | Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵Gravatar Maxime Dénès2017-08-17
|\ \ | | | | | | | | | trailing / and \ on windows)
* \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \
| | * | Removing trailing "/" and "\" in directory names only on win32.Gravatar Hugo Herbelin2017-08-15
| | | | | | | | | | | | | | | | | | | | This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows).
| | | * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|/ |/| | | | | | | | | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
| * | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | |
* | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ | |/ / |/| |
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |/
* | Merge PR #902: Only perform profile initialization and printing when the ↵Gravatar Maxime Dénès2017-07-26
|\ \ | | | | | | | | | flag is set.
* | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |/ |/|
* | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Gravatar Maxime Dénès2017-07-21
| |
* | coq_makefile: use System.exists_dir for better portabilityGravatar Enrico Tassi2017-07-20
| |
* | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)Gravatar Enrico Tassi2017-07-20
| |
| * Also a less intrusive Profile.init_profile.Gravatar Hugo Herbelin2017-07-20
| | | | | | | | | | | | Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible.
| * A less intrusive Profile.close_profile.Gravatar Hugo Herbelin2017-07-20
| | | | | | | | | | | | | | | | | | No need to call Gc functions nor Unix timing functions when there is nothing to report. Moreover, PMP observed problems with these functions in the debugger. PMP also reported that Gc.minor takes some noticeable time, so no need to trigger some when unneeded.
* | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \ | |_|/ |/| |
| | * [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Emilio Jesus Gallego Arias2017-07-19
| |/ |/| | | | | Fix bug introduced by a Haskell programmer.
* | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Gravatar Maxime Dénès2017-07-17
|\ \ | | | | | | | | | rather than colors
| | * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
| * | Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
| |/ | | | | | | | | | | | | | | This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors.
* / use Int.equal instead of polymorphic =Gravatar Paul Steckler2017-07-05
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Fix bug 5392: Warnings defined in plugins are considered unknownGravatar Maxime Dénès2017-06-23
| | | | | | | | | | | | The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning.
* | Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \
* | | Fix typo in comment.Gravatar Maxime Dénès2017-06-19
| | |
| * | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ /
* | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \
* \ \ Merge PR#739: completing a sentence in a commentGravatar Maxime Dénès2017-06-14
|\ \ \
| | * | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Add a version to be used when parsing compatibility notations mentioning old ↵Gravatar Guillaume Melquiond2017-06-14
| |/ / |/| | | | | | | | versions.
* | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
| * | completing a sentence in a commentGravatar Matej Košík2017-06-07
| | |
* | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 11:04:11 +0000