Call for testing: jsUniMath #1729
Replies: 9 comments 6 replies
-
|
It works for me in chrome and not in safari. Looks great! |
Beta Was this translation helpful? Give feedback.
-
|
I tried loading it up in firefox but it seems to be getting blocked and the worker never loads. Relevant info |
Beta Was this translation helpful? Give feedback.
-
|
Thanks for checking! |
Beta Was this translation helpful? Give feedback.
-
|
ah after some investigation, it seems https://coq.vercel.app/ might not run into this issue because they use the |
Beta Was this translation helpful? Give feedback.
-
|
As of this moment, it seems to now run correctly on Firefox for me. The sample seems to evaluate just fine for me and it doesn't look like any errors are being produced in the console. |
Beta Was this translation helpful? Give feedback.
-
|
Hi, I'm also having trouble running it on Windows/ Mozilla. Was there a specific fix in your situation? I also tried on Chrome with similar results. |
Beta Was this translation helpful? Give feedback.
-
|
It works fine (including walking through proofs) for me on Ubuntu 22.04 both with Firefox (version 113.0.1) and Google Chrome (version 114.0.5735.90). Looks nice. I have not yet worked with jsCoq. Is there a way to make the message window bigger? After all, it is supposed to show the statements I have proven. Another curiosity for me: when I do not explicitly import UniMath.CategoryTheory.Core.Categories, the coercions are not applied when viewing statements. Example: See the last lines of the output. |
Beta Was this translation helpful? Give feedback.
-
|
On a related note, is it possible now to create a tutorial page with UniMath like this one: https://cass.pleiad.cl/jscoq/examples/funext/evaluator.html ? |
Beta Was this translation helpful? Give feedback.
-
|
Unfortunately, the tutorial does not function any longer for me (Stack Overflow when defining Expr). The HTML file stems from LaTeX2HTML (as said in the header). But how is the code typed initially? Just as is done for verified Coq code inside a LaTeX document? |
Beta Was this translation helpful? Give feedback.
-
|
macOS (Chrome Version 117.0.5938.92 (Official Build) (arm64)); opening with dark theme (was set automatically, apparently) 
Steps:
|
Beta Was this translation helpful? Give feedback.
-
|
It did not work for me on Windows 10. I tried Mozilla and Chrome. In both cases, it won't load past the screen shown on the screenshot. It just stays there, cursor blinking, not allowing me to use any commands.
|
Beta Was this translation helpful? Give feedback.
-
|
@AlkisIoannidis : thanks a lot for the feedback. I do not know how to fix this, unfortunately :-( |
Beta Was this translation helpful? Give feedback.
-
|
@AlkisIoannidis : to give some more information, we have no knowledge of the workings of jsCoq ourselves. Indeed, I am currently looking for someone who can understand how it works and help me set up a more up-to-date version of jsUniMath. Have you managed to install UniMath on your Windows system, using the Coq platform? |
Beta Was this translation helpful? Give feedback.
-
|
@benediktahrens Thanks for the reply! |
Beta Was this translation helpful? Give feedback.
-
|
Great, thanks for letting us know. Please don't hesitate to get in touch with any questions you have, e.g., on https://unimath.zulipchat.com/. |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
@arnoudvanderleer has set up jsCoq with compiled UniMath (jsUniMath for short) under https://unimath.github.io/live/
For instance, the following code is accepted there:
It would be great if you could test jsUniMath and document things that do, and do not, work there.
In particular:
-type-in-typeThanks a lot to @arnoudvanderleer and to you!
Beta Was this translation helpful? Give feedback.
All reactions