Pierre Courtieu (Jan 04 2021 at 10:38): Pierre Courtieu (Jan 04 2021 at 10:38):Hi there,
Maybe this is known but just in case: in the examples of jscoq lf and plf seem broken: it fails with Cannot open LF
[cannot-open-path,filesystem] + Cannot find a physical path bound to logical path matching suffix
<> and prefix LF.. See for instance: https://x80.org/rhino-coq/v8.11/examples/lf/Induction.html#lab48.
Shachar Itzhaky (Jan 04 2021 at 19:57)::wave: @Pierre Courtieu Did you manage to get https://corwin-of-amber.github.io/sf/src/lf working eventually?
Pierre Courtieu (Jan 05 2021 at 09:30):Yes! Thanks!
But sadly the stack overflow on Search (https://github.com/jscoq/jscoq/issues/215) is a bit of a problem for my use case (students needing to find lemmas).
Shachar Itzhaky (Jan 05 2021 at 10:18):It's not that Search doesn't work altogether, it's that Search with too many results doesn't. I am right now in the process of putting together SF on top of wacoq (https://jscoq.github.io/wa), which does not suffer from this kind of stack overflows.
Last updated: May 31 2023 at 02:31 UTC