Bas Spitters (Nov 10 2022 at 15:27): 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?
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:02):it should be possible I understand
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
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?
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.
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
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:40):you can press Ctrl+Enter to display goals at point
Shachar Itzhaky (Nov 10 2022 at 16:40):that was pretty quick Emilio :)
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:42):yeah just an rsync from the build tree
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
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
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
Shachar Itzhaky (Nov 10 2022 at 16:45):perhaps your server does not like symlinks? Vercel also doesn't like them
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:49):The error is super strange, jsoo version works fine
Shachar Itzhaky (Nov 10 2022 at 16:52):Screenshot-2022-11-10-at-18.52.18.png this?
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):Yup
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):locally with make serve works fine
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:53):puzzling
Shachar Itzhaky (Nov 10 2022 at 16:54):that's Chrome's fault
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:54):maybe it's because the URL?
Shachar Itzhaky (Nov 10 2022 at 16:54):instead of reporting a normal "failed to fetch" it tries to interpret the 404 as wasm
Shachar Itzhaky (Nov 10 2022 at 16:54):welp
Shachar Itzhaky (Nov 10 2022 at 16:54):look at the "network" tab, you will see some wasms are not found
Shachar Itzhaky (Nov 10 2022 at 16:55):my guess is that because they are symlinked
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"])
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:56):I just saw your message, indeed it is because of the url
Emilio Jesús Gallego Arias (Nov 10 2022 at 16:56):let's see where the problem is
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');
in my current setup
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:03):when wacoq comes from installed it should be the latter
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:05):Fixed in the deployment
Shachar Itzhaky (Nov 10 2022 at 17:19):asset uris are the devil
Emilio Jesús Gallego Arias (Nov 10 2022 at 17:31):Yes, as always tooling / build setup takes a huge amount of time
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.
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?
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.
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.
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: Jun 01 2023 at 12:01 UTC