Stream: jsCoq

Topic: Coqdoc as Html in ScratchPad?


view this post on Zulip Bas Spitters (Nov 10 2022 at 15:27):

@Shachar Itzhaky @Emilio Jesús Gallego Arias
In most of jscoq, coqdoc is displayed as html. Is there a way to enable this in the scratchpad?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:02):

it should be possible I understand

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:02):

tho in the branch we work with markdown documents natively, and use prosemirror to display them

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:03):

so depending on your case, it could be better to do that; @Shachar Itzhaky maybe we could deploy the fleche branch with prosemirror somewhere?

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:32):

yes we sort of did not have time to do that. @Bas Spitters what you see in other pages is actually the coqdoc precompiled into HTML and just served statically, which is why the HTML part is not editable. You can ofc compile such documents yourself using jscoqdoc but you will get the same behavior. If you want a document where both the text and the code are editable then the ProseMirror version that Emilio made is the way to go.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:40):

See https://x80.org/rhino-taur/?frontend=pm&content_type=plain or just https://x80.org/rhino-taur

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:40):

you can press Ctrl+Enter to display goals at point

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:40):

that was pretty quick Emilio :)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:42):

yeah just an rsync from the build tree

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:42):

I've push a little commit to set the frontend by url, seems much more practical

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:42):

I'm puzzled tho the wa backend works locally but not on my server, mmm

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:44):

oh there are symlinks in node_modules, it's a very bad hack I'm trying to get rid of

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:45):

perhaps your server does not like symlinks? Vercel also doesn't like them

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:49):

The error is super strange, jsoo version works fine

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:52):

Screenshot-2022-11-10-at-18.52.18.png this?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):

Yup

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):

locally with make serve works fine

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):

puzzling

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:54):

that's Chrome's fault

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:54):

maybe it's because the URL?

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:54):

instead of reporting a normal "failed to fetch" it tries to interpret the 404 as wasm

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:54):

welp

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:54):

look at the "network" tab, you will see some wasms are not found

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:55):

my guess is that because they are symlinked

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:56):

oh yes, maybe this is suspicious ? await this.core.run("/lib/icoq.bc", [], ["wacoq_post"])

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:56):

I just saw your message, indeed it is because of the url

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:56):

let's see where the problem is

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:02):

I think this line should be

    var icoq = new IcoqPod('../backend/wasm', '../node_modules');

instead of

    var icoq = new IcoqPod('../backend/wasm', '../../../node_modules');

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:03):

in my current setup

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:03):

when wacoq comes from installed it should be the latter

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:05):

Fixed in the deployment

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 17:19):

asset uris are the devil

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 17:31):

Yes, as always tooling / build setup takes a huge amount of time

view this post on Zulip Bas Spitters (Nov 11 2022 at 10:39):

@Emilio Jesús Gallego Arias That looks pretty impressive!
I got confused for a minute by the cursor placement. If I put my cursor after rewrite IHl. It says "No more goals."
I would expect this to only happen after putting my cursor after the r of reflexivity.

view this post on Zulip Bas Spitters (Nov 11 2022 at 10:41):

Is there a way to take an existing Coqdoc file and convert it into markdown to be used in rhino?

view this post on Zulip Shachar Itzhaky (Nov 11 2022 at 10:46):

Bas Spitters said:

Emilio Jesús Gallego Arias That looks pretty impressive!
I got confused for a minute by the cursor placement. If I put my cursor after rewrite IHl. It says "No more goals."
I would expect this to only happen after putting my cursor after the r of reflexivity.

yes, this is precisely the kind of UI design choices that we still need to make before the Fleche model is usable. This is good feedback, we know that the current goal display is not intuitive yet; what we have now was mostly for us to test that we can extract and print goals properly.

view this post on Zulip Shachar Itzhaky (Nov 11 2022 at 10:47):

a coqdoc → markdown translation sounds like it would be useful; perhaps Alectryon has this capability? I remember @Clément Pit-Claudel mentioning bidirectional translation in that area.

view this post on Zulip Bas Spitters (Nov 11 2022 at 12:07):

Yes, that would be useful. I'd imagine we may want to deprecate coqdoc syntax at some point and use something standard.


Last updated: Jan 30 2023 at 17:03 UTC