Stream: jsCoq

Topic: lf and plf jscoq examples broken


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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: Jan 30 2023 at 16:03 UTC