Stream: jsCoq

Topic: jscoq and the reals


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:37):

Hi @Laurent Théry , AFAICT the tactics should work, modulo bugs

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:39):

you can try on the main demo page

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:39):

Contains the reals and plugins, etc...

view this post on Zulip 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/.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:40):

You can have a look at the package file if you are curious, but these days loading is automatic

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:43):

We used to have flocq actually

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:44):

should be pretty easy to add to https://github.com/jscoq/addons

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:44):

unfortunately the addons system is still in development :S

view this post on Zulip 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?

view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC