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 02 Feb 2011 10:04:00 AM UTC  
 
Category: DevelopmentModule: BiCoax
Priority: 1 - LaterSeverity: 1 - Wish
Status: Need InfoPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Wed 02 Feb 2011 06:29:13 PM UTC, 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 02 Feb 2011 10:04:00 AM UTC, original submission:

Hello,

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 ;)

Thanks

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.

     

    Please enter the title of George Orwell's famous dystopian book (it's a date):

     

     

    Follows 1 latest change.

    Date Changed By Updated Field Previous Value => Replaced By
    Wed 02 Feb 2011 06:29:13 PM UTCscolinStatusNone=>Need Info
    Show feedback again

    Back to the top


    Powered by Savane 3.1-cleanup