aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
...
* | | | | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | coq_makefile are in sync (supersed #1039)…
| | | | * | [pp] Minor optimization in `Pp.t` construction and gluing.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
| | | | * Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | |
| | | | * Distinguishing pseudo-letters out of the set of unicode letters.Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
| | | | * Fixing typos in comments of unicode.ml.Gravatar Hugo Herbelin2017-10-05
| | | | |
* | | | | Merge PR #1100: Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1015: Adding a function to be typically used to pass values from ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | | | | | | | | an OCaml "when" clause to the r.h.s of the matching clause
| | * | | | Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-09-27
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open.
| | | | * Improve support for "-w none" compatibility option.Gravatar Guillaume Melquiond2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If coqtop was started with "-w none" yet the script used "Set Warnings Append", then all the warnings were turned back to their default value. This commit turns "none" (whatever its sign) into "-all" whenever some warning status is modified afterward, in order to prevent the issue.
| | * | | coq_makefile: make sure compile flags for Coq and coq_makefile are in syncGravatar Emilio Jesus Gallego Arias2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
* | | | | Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
| |_|_|/ |/| | |
* | | | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
| | | |
| | | * 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
| |_|/ |/| |
| * | Adding function to be typically used to pass values from an OCaml "when" clause.Gravatar Hugo Herbelin2017-09-12
|/ /
* | 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:34:07 +0000