bugBRILLANT - Bugs: bug #17630, A bicoax-coqtop

Show feedback again

You are not allowed to post comments on this tracker with your current authentification level.

bug #17630: A bicoax-coqtop

Submitted by:  Georges Mariano <gmariano>
Submitted on:  Wed Feb 2 10:04:00 2011  
Category: DevelopmentModule: BiCoax
Priority: 1 - LaterSeverity: 1 - Wish
Status: Need InfoPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Wed Feb 2 18:29:13 2011, comment #1:

There is a coqmktop, but it is decicated to the inclusion of ocaml-programmed tactics (i.e., not embedding already stored theorems). I think it is not possible to do so.

a) Hard to say. As Blib is already compiled, it just has to load it and maybe ensure it is well-formed, so it does not take much time.

b) coqtop and coqide have much in common, but are different executables : any procedure to create a coqtop with a preloaded Blib would have to be replicated with coqide.

The best way of knowing if something can be improved speedwise would be to experiment with the various coqtop options (such as -dont-load-proofs).

Samuel Colin <scolin>
Project AdministratorIn charge of this item.
Wed Feb 2 10:04:00 2011, original submission:


Would be nice to have a dedicated bicoax coqtop ...

That is a coq toplevel with a preloaded Blib.

This way we should avoid to load the Blib library each time we call coq.

a) I'm not sure that it will save really lot of time, don't know exactly...

b) is this compatible with the use of coqide ? (more exactly, the reverse question : is this allowed by coqide)

Priority : low ;)


Georges Mariano <gmariano>
Project Administrator


No files currently attached


Depends on the following items: None found

Items that depend on this one: None found


Carbon-Copy List
  • -unavailable- added by scolin (Posted a comment)
  • -unavailable- added by gmariano (Submitted the item)

    Do you think this task is very important?
    If so, you can click here to add your encouragement to it.
    This task has 0 encouragements so far.

    Only logged-in users can vote.


    Error: not logged in



    Follows 1 latest change.

    Date Changed By Updated Field Previous Value => Replaced By
    Wed Feb 2 18:29:13 2011scolinStatusNone=>Need Info
    Show feedback again

    Back to the top

    Powered by Savane 3.1-cleanup