Laurent Théry (Oct 19 2020 at 10:27): Laurent Théry (Oct 19 2020 at 10:27):I would be interested to use jscoq and the Reals library. When looking at the section What is broken.
What is broken
Loading ML modules is slow.
Loading .vo files is slow.
There surely are threading and performance problems.
vm_compute and native_compute fall back to regular compute.
does that mean that I will have to do without the tactics like ring and lra?
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:37):Hi @Laurent Théry , AFAICT the tactics should work, modulo bugs
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:39):you can try on the main demo page
Laurent Théry (Oct 19 2020 at 10:39):I have seem that there is a package coq-reals how do I know what it contains
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:39):Contains the reals and plugins, etc...
Karl Palmskog (Oct 19 2020 at 10:39):I tried the following on https://jscoq.github.io which might not be up-to-date:
From Coq Require Import Lia.
Lemma bla : forall x : nat, x > 10 \/ x <= 10.
Proof.
lia.
Qed.
However, I get the following at the Qed.:
Anomaly
"Uncaught exception Error: vm trap: 'coq_set_bytecode_field' not implemented."
Please report at http://coq.inria.fr/bugs/.
You can have a look at the package file if you are curious, but these days loading is automatic
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:41):@Karl Palmskog that indeed seems like a bug in the build, @Shachar Itzhaky did we pass the right configure options?
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:41):If you go to the 8.11 version at https://x80.org/rhino-coq/ it works
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:42):it should be easy to solve, it is either a build problem or some bug in 8.12 that we can patch
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:43):https://github.com/coq/coq/issues/12655 makes it hard to test that there are no regressions in this front
Laurent Théry (Oct 19 2020 at 10:43):@Emilio Jesús Gallego Arias I have tried it seems to work. So my first step is to build an addon for flocq if I need it
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:43):We used to have flocq actually
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:44):should be pretty easy to add to https://github.com/jscoq/addons
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:44):unfortunately the addons system is still in development :S
Laurent Théry (Oct 19 2020 at 12:45):I was trying to follow https://github.com/jscoq/jscoq/blob/v8.12/docs/build.md#building-accompanying-libraries-optional so it will not work?
Emilio Jesús Gallego Arias (Oct 19 2020 at 12:54):It should but definitively @Shachar Itzhaky is the ultimate authority on whether things are still up to date :)
Laurent Théry (Oct 20 2020 at 09:24):i am stuck at step 7 of https://github.com/jscoq/jscoq/blob/v8.12/docs/build.md#building-accompanying-libraries-optional .
When trying to build the mathcomp addon it says
12 | (run jscoq build %{dep:coq-mathcomp.json} --package coq-pkgs/mathcomp)))
^^^^^
Error: Program jscoq not found in the tree or in PATH
where this jscoq command is supposed to be built?
Shachar Itzhaky (Oct 20 2020 at 16:43):I thought that I changed it to (run npx jscoq ... everywhere. But mathcomp is the most "senior" of the addons, I must have missed it.
Shachar Itzhaky (Oct 20 2020 at 16:43):(for me it works because I use npm link to test jsCoq, so the command is linked from my PATH...)
Shachar Itzhaky (Oct 20 2020 at 16:46):Karl Palmskog said:
I tried the following on https://jscoq.github.io which might not be up-to-date:
From Coq Require Import Lia. Lemma bla : forall x : nat, x > 10 \/ x <= 10. Proof. lia. Qed.However, I get the following at the
Qed.:Anomaly "Uncaught exception Error: vm trap: 'coq_set_bytecode_field' not implemented." Please report at http://coq.inria.fr/bugs/.
Cheers @Karl Palmskog , this is indeed a bug where Coq was ignoring our configure flag; we have fixed it already (https://github.com/jscoq/jscoq/issues/201) but have not made a release since. I think now would be a good time to make a 0.12.1 release.
Shachar Itzhaky (Nov 09 2020 at 11:03):I've put up a release candidate for 0.12.1. So this fix is now live.
Last updated: May 31 2023 at 02:31 UTC