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 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.
:wave: @Pierre Courtieu Did you manage to get https://corwin-of-amber.github.io/sf/src/lf working eventually?
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).
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