Fix some issues in refman

[ia0]

No description provided.

[jfehrle]

Your changes look fine. I can merge as is if you wish. If you're willing to do a little more, how about adding a working example?

On line 70, lvar is not defined. It's probably the list passed in variables.

FWIW Looking through the code pretty thoroughly, I can't find where parameters such as radicalmax are parsed. Also I think we could do better then using 1%Z etc for strategy.

[ia0]

Your changes look fine. I can merge as is if you wish. If you're willing to do a little more, how about adding a working example?

I tried to add the first example from the test-suite/success/Nsatz.v file (by the way the link was broken since stdlib moved to its own repo), but I failed. Here is what I tried:

   .. example::

      .. rocqtop:: all extra-stdlib

         From Stdlib Require Import NsatzTactic.
         Goal forall (x y z : Z),
             x + y + z = 0 -> x*y + x*z + y*z = 0 -> x*y*z = 0 ->
             x*x*x = 0.
         nsatz.

And I get this error:

Error: Cannot find a physical path bound to logical path NsatzTactic with prefix Stdlib.

I thought the extra-stdlib would take care of this, but maybe it doesn't provide access to the whole stdlib. So maybe we can't really do better than link to the stdlib test-suite as currently done.

On line 70, lvar is not defined. It's probably the list passed in variables.

I also don't know. I didn't read too much into that paragraph. I'm not planning to use nsatz, I'm just reading through to know what exists and what can be done with it.

[SkySkimmer]

"extra" means optional, so it will ignore errors unless env variable ROCQRST_EXTRA is used. The idea is that when stdlib is installed you use ROCQRST_EXTRA=stdlib to catch errors in the extra-stdlib sections, and when it's not you can still compile the refman by tolerating errors in the extra-stdlib sections.
CI builds the refman with ROCQRST_EXTRA=all (and stdlib etc installed) in the ci-refman job.

[SkySkimmer]

rocq/doc/sphinx/README.rst

Line 259 in 2865a49

- ``extra-foo``: if environment variable 'ROCQRST_EXTRA' is set to `all`

[ia0]

CI builds the refman with ROCQRST_EXTRA=all (and stdlib etc installed) in the ci-refman job.

Should I use the CI scripts to test locally? (most probably using Makefile.ci)

Because if I use ROCQRST_EXTRA=all make refman-html after make world I still get the failure because Stdlib is in a different repository without any submodule logic. I tried to find documentation explaining how to locally compile stdlib from the rocq repository but couldn't.

[SkySkimmer]

You can try doing make ci-stdlib between world and refman.
Not sure if it works as the ci-refman job has some sed hacks.

[SkySkimmer]

If it gets too annoying just ask us to run full CI

[ia0]

You can try doing make ci-stdlib between world and refman. Not sure if it works as the ci-refman job has some sed hacks.

make ci-stdlib works, but it builds under _build_ci which might not be used by make refman-html because NsatzTactic is still not found. I tried make ci-refman but this requires more installed dependencies. If there is no simple way to build the refman locally with stdlib that's fine. I shouldn't need to do it too often.

[SkySkimmer]

make ci-stdlib also installs (in _build/install/...). However dune may be deleting the installed files in the next build command.

[ia0]

make ci-stdlib also installs (in _build/install/...). However dune may be deleting the installed files in the next build command.

Indeed:

% make ci-stdlib
[...]
% find _build -name NsatzTactic.vo
_build/install/default/lib/coq/user-contrib/Stdlib/nsatz/NsatzTactic.vo
% ROCQRST_EXTRA=all make refman-html
[...]
% find _build -name NsatzTactic.vo
%

[SkySkimmer]

@coqbot run full ci

[ia0]

Weird, the tactic fails:

Toplevel input, characters 0-5:
> nsatz.
> ^^^^^
Error: Tactic failure: Proof search failed.

But rocq c foo.v works with Rocq version 9.0.0 and foo.v being:

From Stdlib Require Import NsatzTactic.
Goal forall (x y z : Z),
    x + y + z = 0 -> x*y + x*z + y*z = 0 -> x*y*z = 0 ->
    x*x*x = 0.
nsatz.
Abort.

[SkySkimmer]

try From Stdlib Require Import Nsatz instead

[SkySkimmer]

(probably changed in rocq-prover/stdlib#155)

[Zimmi48]

Why is the CI job green if the tactic failed? Is this a bug of the extra parameter?

[ia0]

Why is the CI job green if the tactic failed? Is this a bug of the extra parameter?

I've noticed this locally. Without extra-stdlib, make refman-html completes without error. There's only the error message in the rendered HTML. So I guess it's the same reason why even with extra-stdlib errors are not reported to the build command line.

[jfehrle]

Why is the CI job green if the tactic failed? Is this a bug of the extra parameter?

It sounds like errors in .. rocqtop blocks don't return failure status to the refman process (and cause a build failure). We could add that, but if there are blocks that are supposed to end with a failure status, we would may need an "ignore_error" flag on the block so the refman build won't fail in those exceptional cases.

When I try to build locally, the refman job is not finding stdlib :-(

But if I run rocqide locally (dune exec -- rocqide) , it does find stdlib:

(Tested on master from maybe a month ago.)

[SkySkimmer]

if there are blocks that are supposed to end with a failure status, we would may need an "ignore_error" flag on the block

we already have that, it's called "fail"

[jfehrle]

@ia0 I'm just reading through to know what exists and what can be done with it.

You probably already know that there are many external libraries that are not documented in the refman. (I've never looked at them; I'm not a typical user of Rocq.)

[ia0]

I suggest to delete the last 2 commits (essentially not adding any example and only fixing immediate issues). The link to the stdlib test-suite seems enough and the rocqtop-to-refman failure propagation issue is orthogonal (but should probably be addressed).

What do you think?

[Zimmi48]

the rocqtop-to-refman failure propagation issue is orthogonal (but should probably be addressed).

I opened an issue about this: #21010.

[jfehrle]

Let's declare victory.

@coqbot: merge now

Thanks for the PR!