Huỳnh Trần Khanh (Nov 24 2022 at 12:02): Huỳnh Trần Khanh (Nov 24 2022 at 12:02):now, looks like jscoq also suffers from this! i got
Anomaly "Uncaught exception SyntaxError: Invalid regular expression: /maximum call stack/: Maximum call stack size exceeded."
Please report at http://coq.inria.fr/bugs/.
could anyone look into this? or is this something that we should just live with because jscoq has more severe limitations?
Shachar Itzhaky (Nov 24 2022 at 12:05):it's a stack overflow and there's not much to do because typechecking is not tail recursive and the JS stack is limited. We are gradually shifting towards the WASM backend (https://coq-next.vercel.app/wa/)
Shachar Itzhaky (Nov 24 2022 at 12:09):I tried @Michael Soegtrop's example in waCoq and it gets stuck so perf-wise I think the problem exists.
Shachar Itzhaky (Nov 24 2022 at 12:16):@Emilio Jesús Gallego Arias Maybe the right thing to do is to just limit the size of the term that is being processed. At least, waCoq does display the same formula as CoqIDE for small constants (which according to https://github.com/coq-community/vscoq/issues/317, VSCoq does not). We might be able to get away with a character limit for the printer (and a '...' button in case you are really willing to go through damnation to print the entire 4000 lines).
Emilio Jesús Gallego Arias (Dec 06 2022 at 13:46):@Shachar Itzhaky indeed, it'd be great to improve this, but note that printing is involved and the performance bottleneck may happen well before the printer itself. For a goal to be printed, Coq needs to do:
I'd bet that there are some super-linear code in steps 1 / 2 (and maybe even 3)
The ... button is a great idea, but I'm still thinking how to best implement it, Lean's infoview have a RPC to manage lifetimes which I'd rater avoid as state management becomes complex; memoization could work better IMVHO but we need to try.
Anyways I'd suggest to advance on this topic on the coq-layout-engine branch with perf tests.
Last updated: Jan 31 2023 at 10:01 UTC