aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13940 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
- During input and output to coqide, we postpone Ctrl-C instead of ignoring them. For that we use Util.interrupt and Util.check_for_interrupt. - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break, which is more reliable than waiting for the next Util.check_for_interrupt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Coqide: synchronise the reset_initial via the coq_computing mutexletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13938 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakletouzey
Default behavior for (Sys.catch_break false) is to exit, while we want the opposite: survive. When I write an ad-hoc catch_break, I'd better use it, damnit ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13937 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: restaure compilation of ide/macjokes.c removed by mistakeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13936 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: misc (nicer message than End_of_file, a useless try removedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave: improved handling of exceptions (in particular ^C)letouzey
we try to ignore ^C during I/O but enable it during treatment of requests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13934 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide_slave: a more robust current_status () functionletouzey
- Due to -top foobar, or -notop, the current dir_path () doesn't necessary starts by Top. - Start documenting Ide_intf git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13933 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-28Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsletouzey
* Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25ide/coqide.ml: a pass of more decent automatic indentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13931 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide: more reorganisation and cleanupletouzey
- Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide_intf : change type of location in ideletouzey
We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide: mention "Restart" instead of "Go to start" for corresponding buttonletouzey
This way probably emphasizes more the fact that the coqtop subprocess is killed and a new one is spawned. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13928 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23Ide: stronger separation from coqtopletouzey
Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23Ide: experimentally allow coqide to interrupt or kill coqtopletouzey
- We now use create_process instead of open_process, and stores the answered pid. - The "Stop" button now sends a Sigint signal to this coqtop pid. - The "Goto Start" button now works even if a computation is ongoing, a new process is spawned and the previous one is killed -9, and then a waitpid is done to avoid having zombies around. Note that currently a vm_compute won't be stopped by a "Stop", but only by a "Goto Start". This can be quite confusing. How to properly document that "Goto Start" has the side effect of being a kill ? Maybe we could check someday if the Ctrl-C has been successful, and kill -9 if not ? Or maybe make coqide aware of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C in this case ? TODO: - for the moment a forced "Goto Start" displays an unfriendly anomaly - check if all this works under Windows (probably but not sure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23- Remove useless grammar rulemsozeau
- Better printing of unif constraints in evar_map's git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13925 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong ↵msozeau
environment sometimes. - Remove compilation warning in classes.ml due to (as yet) unused code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13924 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Init: some results in Type should rather be Defined than Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13920 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-21Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsletouzey
This was breaking the FireSquad extraction test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13919 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-18Makefile.build: compile the stdlib with -dont-load-proofs by defaultletouzey
Since library files aren't meant to contain queries like Print Assumptions nor extractions, it is safe (and quite quicker) to compile them with -dont-load-proofs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13918 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
Note: even if this new tactical can be quite handy during the development phase, (for instance to bound the time allocated to some search tactics), please be aware of its main drawback: with it, scripts are no longer machine-independant, something that works on a quick machine may fail on a slow one. The converse is even possible if you combine this "timeout" with other tactic combinators. We strongly advise to not leave any "timeout" in the final version of a development. In addition, this feature won't probably work on native win32, since Unix.alarm isn't implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13917 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17An option "Set Default Timeout n."letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17Goptions: repair Unset for int optionsletouzey
Previous code was trying to do a bool write, and in case of error, a int write. But for compatibility reason, bool write error were turned into warnings, preventing Unset Foo Bar to work when Foo Bar is an int option. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13915 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y), (Plt=lt x y) (Pgt=lt y x), but this may not be always the case, especially for Pgt. The former CompSpec is now defined in term of CompareSpec. Compatibility is preserved (except maybe a rare unfold or red to break the CompSpec definition). Typically, CompareSpec looks nicer when we have infix notations, e.g. forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x) while CompSpec is shorter when we directly refer to predicates: forall x y, CompSpec eq lt x y (compare x y) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Adapt printers.mllib after my last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13913 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Finish branching functions handling module errors (cf. r13886)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13912 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
Probably something related with the unicode lambda syntax... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13911 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13910 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
in preparation for adding forward reasoning to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Inference of match predicate produces ill-typed unification problem,msozeau
revert to manual building of the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13906 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11- Better error messages taking unif. constraints into account.msozeau
- Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
- In clenv, this used to forget the existing constraints, there are none in the other evar_map. - Other uses (evar_refiner, class_tactics) always reset with an enriched version of the same evar_map. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13901 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditionsletouzey
Initial patch by Robbert Krebbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13900 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Solve evar instantiations in the right environment.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13899 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Fix declarations of [Add Setoid/Morphism...] in sections to not exportmsozeau
by default (bug introduced in r13842). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13898 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08syntax for exponentspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13897 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08adding eta in the vmbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
be unified with a (truly) rigid term would need to be able to project non-atomic arguments of evars what is not done (consider e.g. "Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n))."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13892 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: fix printing of haskell modular namesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13890 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
This happens for instance when the main component of the fixpoint block has been provided via Extract Constant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13889 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07A new command "Separate Extraction"letouzey
This is a mix of "Recursive Extraction" and "Extraction Library": - like "Extraction Library", the extracted code is splitted in separated files, one per coq source file. - unlike "Extraction Library", but similarly to "Recursive Extraction", not everything gets extracted, but only dependencies of some initially-given elements We prepare for a more clever dependency selection inside sub-modules. For the moment all needed sub-modules are still fully extracted (other we would need to fix signatures accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13888 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:43:47 +0000