Custom Query (361 matches)
Results (46 - 48 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #139 | fixed | Prover not started when run from Product | ||
| Description |
Prover does not start when run from a Product configuration, though it starts successfully as a plugin. Exception seems to be generated by the system path management which calls the prover and its tools. |
|||
| #140 | fixed | PG takes a long time printing module types in Coq | ||
| Description |
Dear Proof General developers, I found a curious behavior: it seems that the time it takes PG to print the module type in Coq grows exponentially (or faster?) depending on the number of parameters in this module type. For example, I started with Module Type T. Parameter p1 : nat. End T. and started adding lines "Parameter p2 : nat.", "Parameter p3 : nat.", etc. Each time I issued the command Time Print Module Type T. after the closing of the module type T. Up to 4 parameters were printed practically instantaneously. When T had 5 parameters, the printing command took about 5 seconds, and when it had 6 parameters, it took about 60 seconds. In all cases the time requires by Coq as printed by the "Time" command was negligible (~ 0.001 s.). Also, I tried entering all these commands directly in coqtop, and again, printing was instantaneous. |
|||
| #143 | fixed | Add XML/PGIP test scripts to Isabelle/Admin distribution | ||
