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`

?

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

you can try on the main demo page

I have seem that there is a package `coq-reals`

how do I know what it contains

Contains the reals and plugins, etc...

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

@Karl Palmskog that indeed seems like a bug in the build, @Shachar Itzhaky did we pass the right configure options?

If you go to the 8.11 version at https://x80.org/rhino-coq/ it works

it should be easy to solve, it is either a build problem or some bug in 8.12 that we can patch

https://github.com/coq/coq/issues/12655 makes it hard to test that there are no regressions in this front

@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

We used to have `flocq`

actually

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

unfortunately the addons system is still in development :S

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?

It should but definitively @Shachar Itzhaky is the ultimate authority on whether things are still up to date :)

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?

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.

(for me it works because I use `npm link`

to test jsCoq, so the command is linked from my PATH...)

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.

I've put up a release candidate for 0.12.1. So this fix is now live.

Last updated: Oct 13 2024 at 01:02 UTC