Custom Query (361 matches)

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...

Proof general seems to stall when trying to evaluate very long (textually long) ltac declarations. See example at the end. If you remove a line or two of the "let x := match ... in" then there is no problem. Is there a limit to the size of expressions that are fed to Coq?

Ltac bar k := k tt.

Ltac foo x := 
  bar ltac:(fun a => 
  bar ltac:(fun b => 
  bar ltac:(fun c => 
  bar ltac:(fun d => 
  bar ltac:(fun e => 
  bar ltac:(fun f => 
  bar ltac:(fun g => 
  bar ltac:(fun h => 
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  let x := match tt with | tt => constr:(1) end in
  idtac)))))))).

I have the following error at compile time:

generic/pg-response.el:104:23:Error: special-display-regexps' is an obsolete variable (as of 24.3); use display-buffer-alist' instead.