aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16704 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-12Fixing potentially misused Errors.push.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16699 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-10Printing any backtrace in debug mode, not only anomalies.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16696 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-10Small typosppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-09checker validation fixed w.r.t. Futuresgareuselesinge
still not working, it complains about the universe constraint set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-09state_id data typegareuselesinge
(this should have been the first commit of Paral-ITP) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16688 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
Stm contains many TODO items to improve the thing, but it should be already possible to play with it (but not use it in production). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08State Transaction Machinegareuselesinge
The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Vcs data structure (Git inspired builder for Dag)gareuselesinge
Given named branches, one can incrementally build a Dag using Git like commands git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16672 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Dag data structuregareuselesinge
This is a very simple, only growing, Dag structure with per node optional info and per edge info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16671 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Searchable stack data structuregareuselesinge
It is like Stack but one can search without popping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Future library to represent pure computationsgareuselesinge
Since the whole system is imperative, futures are run protecting the global state, and the final state is also saved to let the user freely chain futures. Futures can represent local (lazy) computations or remote ones (delegated). Delegating a future lets a third party assign its value at some poit in the future; in the meanwhile accessing the future value raises an exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Small fix in IStream interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
parametric on the list of possible flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16665 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05Removing SortArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-30Using functors to reduce the boilerplate used in registeringppedrot
generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Getting rid of IntroPatternArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Splitted up Genarg in four different levels:ppedrot
1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Changing the type of Ltac values. Now they are toplevel genericppedrot
arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Quite ad-hoc for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-02Flags V8_4 for compatibility infrastructure.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16555 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-29More clever implemenation for IStream.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16538 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16537 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28Adding a persistent stream data structure.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-23Fixing #3042ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16530 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16Fixing Pp.strbrk which was reversing words.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16529 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16std_ppcmds is persistent, errors can be printed twicegareuselesinge
The patch is very simple and naive, there is no lazy involved. This makes a difference only for strbrk. An extra patch may be necessary if there is a noticeable slowdown. In any case the data type used is opaque, to ease any future optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16528 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Gmap is now useless, hail to Map!ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16523 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-14Removing Fmap from libraries, it is not used anymore.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16519 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing Fset, since it is not used anymore.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16515 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing the use of Fset/Fmap from Trie. There was actually onlyppedrot
one place depending on fold order, which was easy to bypass. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16514 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
exactly once at runtime, often to reduce the mutual dependency of modules. This module permits to track them more easily. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Documenting the Tries module, uniformizing the names according toppedrot
Map/Set style and renaming the file accordingly as Trie. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16504 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Getting rid of module Gmapl.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-09Xml_datatype.mli ships the xml typegareuselesinge
This breaks the dependency of Xml_parser, Xml_printer and Xml_utils on Serialize. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16493 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Fixing ocamldoc compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16483 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
full usage of notations instead of the previous cheap way to prevent circularity in printing by deactivating all notations. (Since "->" became a notation, printing abbreviations without notations at all had become even more inconvenient). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16454 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Fix indentationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16450 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:11:19 +0000