Hello,
I tried proofgeneral on the newly released emacs and it works at first sight
but seems to have some problems with long input, like the one produced by this
bash script:
function mk { echo "Check fun n, match n with "; s=O; for ((i=0;i<$1;i++)); do
echo " | $s => n"; s="(S $s)"; done; echo " | _ => n end."; } > x.v
Processing x.v for small arguments like
$ mk 10
works but for bigger ones like
$ mk 100
it blocks without consuming cpu.
Weirdly for me the threshold seems to be 42...
--
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
