aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixed "Eval ... in t" when t has still metavariables.Gravatar herbelin2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
| | | | | | | - Missing space and bad constr level in "About f" - Display of arguments missing when used as a pattern notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: unfolds the let-in created by Program when handling "match"Gravatar letouzey2011-04-07
| | | | | | | | | | | This leads to code closer to the original input of the user, and moreover some more dummy __ may be removed this way. To avoid unfolding by mistake user's variables, we change the name of these generated let-in into "program_branch_NN" instead of "branch_NN" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid some useless Obj.magic by fixing my ML type unifierGravatar letouzey2011-04-07
| | | | | | | | | | | Due to wrong pattern order in Mlutil.mgu, simple situations like ?n == ?n were considered unsolvable as soon as one side was aliased (i.e. inside an instantiated type meta). Moreover, use general equality as last resort, instead of forgetting cases like Taxiom == Taxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
| | | | | | (backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix dev/base_include after change of constant_bodyGravatar letouzey2011-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13958 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.Gravatar aspiwack2011-04-06
| | | | | | Patch submitted by Tom Prince. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
| | | | | | | | | This is useful, for example, in declaring the projection of the dependent record bundled form of an unbundled typeclass. Patch submitted by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix last commit about coqdep: not everyone has a user-contrib dirGravatar letouzey2011-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13953 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quickly avoid global axioms in Loic new files about ringGravatar letouzey2011-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adjust coqdep so that it behaves like coqtop with respect to the ↵Gravatar gmelquio2011-04-01
| | | | | | | | | | user-contrib directory. In particular, this directory should be traversed recursively and the full name of its libraries should not be prefixed by the "Coq" logical path. This fixes coqdep spamming the following message while the yyy library is in the user-contrib loadpath. *** Warning: in file xxx.v, library yyy.v is required and has not been found in loadpath! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13949 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
| | | | | | | | | | | | | | | | | | We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13946 85f007b7-540e-0410-9357-904b9bb8a0f7
* As remarked by Enrico, we'd better use eq_constr than structural equalityGravatar herbelin2011-03-31
| | | | | | | (it is a priori optimized but also able to reason modulo equality of names and modulo alpha-conversion). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: customized inductives are always standardGravatar glondu2011-03-31
| | | | | | | If the user customized the inductive, he should know what he is doing... This (hopefully) fixes bug #2482. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)Gravatar letouzey2011-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: avoid confusion of process when restarting coqtop + cosmeticGravatar letouzey2011-03-30
| | | | | | | | | | | | | | | | | | | When using "Goto start" while many phrases are evaluated, it's frequent with earlier code that the restart occurs between two phrases, and hence the second is sent to the new coqtop, triggering things like "Anomaly: NoCurrentProof". To avoid that, Coq.coqtop is now immutable (no silent switch of channels). In Coqide, toplvl and mycoqtop are now references, that are updated when using reset_coqtop. We organize things in order to have only one access to mycoqtop during code that does many sequential calls to coqtop. This way, when coqtop changes, the code speaks to the old one, and gets some exception when writing/reading on a close channel. By the way, some documentation, cleanup, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_intf: documentation of calls + debug printing of calls/answersGravatar letouzey2011-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_intf: remove useless int answer to the "interp" and "rewind" callsGravatar letouzey2011-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
| | | | | | | | | - 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
* Coqide: synchronise the reset_initial via the coq_computing mutexGravatar letouzey2011-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakGravatar letouzey2011-03-28
| | | | | | | | 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
* Ide: restaure compilation of ide/macjokes.c removed by mistakeGravatar letouzey2011-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: misc (nicer message than End_of_file, a useless try removedGravatar letouzey2011-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave: improved handling of exceptions (in particular ^C)Gravatar letouzey2011-03-28
| | | | | | | 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
* Ide_slave: a more robust current_status () functionGravatar letouzey2011-03-28
| | | | | | | | - 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
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
| | | | | | | | | | | | | * 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
* ide/coqide.ml: a pass of more decent automatic indentationGravatar letouzey2011-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13931 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - 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
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
| | | | | | | 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
* Ide: mention "Restart" instead of "Go to start" for corresponding buttonGravatar letouzey2011-03-25
| | | | | | | 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
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | 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
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | | | | | | | | | - 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
* - Remove useless grammar ruleGravatar msozeau2011-03-23
| | | | | | - 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
* - Fix solve_simpl_eqn which was cheking instances types in the wrong ↵Gravatar msozeau2011-03-23
| | | | | | | | 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
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init: some results in Type should rather be Defined than QedGravatar letouzey2011-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsGravatar letouzey2011-03-21
| | | | | | 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
* Makefile.build: compile the stdlib with -dont-load-proofs by defaultGravatar letouzey2011-03-18
| | | | | | | | 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
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
| | | | | | | | | | | | | | 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
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
| | | | | | | | | 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
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
| | | | | | | | | | | | | | | | | | | 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
* Adapt printers.mllib after my last commitGravatar letouzey2011-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish branching functions handling module errors (cf. r13886)Gravatar letouzey2011-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)Gravatar letouzey2011-03-16
| | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-29 22:46:21 +0000