masters/rusthornbelt:README.md lists outdated prerequisites

I tried to follow README.md in masters/rusthornbelt and observed the following.

I think the prerequisite section of the README can be updated. I'm attaching a patch that fixes the situation for me.

Observation: coq-iris dev.2022-04-12.0.a3bed7ea is not compatible with coq-lambda-rust-builddep

% opam pin add coq-iris --current
coq-iris is now pinned to git+https://gitlab.mpi-sws.org/iris/iris.git#a3bed7ea1a562ab41e5479744c249d7b2e16d7f7 (version dev.2022-04-12.0.a3bed7ea)
% make build-dep
# Installing builddep packages.
[coq-lambda-rust-builddep.dev] synchronised (no changes)
[ERROR] Package conflict!
  * Missing dependency:
    - coq-lambda-rust-builddep → coq-iris (= dev | = dev.2025-03-25.0.79d33e24)
    not available because the package is pinned to version dev.2022-04-12.0.a3bed7ea

No solution found, exiting
make: *** [builddep] Error 20

Observation: coq 8.15.0 is not compatible with coq-lambda-rust-builddep

% opam pin remove coq-iris
Ok, coq-iris is no longer pinned to git+https://gitlab.mpi-sws.org/iris/iris.git#a3bed7ea1a562ab41e5479744c249d7b2e16d7f7 (version dev.2022-04-12.0.a3bed7ea)
Nothing to do.
% make build-dep
# Installing builddep packages.
[coq-lambda-rust-builddep.dev] synchronised (no changes)
[ERROR] Package conflict!
  * Missing dependency:
    - coq-lambda-rust-builddep → coq-iris (= dev | = dev.2025-03-25.0.79d33e24) → coq >= 8.19
    not available because the package is pinned to version 8.15.0

No solution found, exiting
make: *** [builddep] Error 20

Observation: coq 8.20.0 works

% opam pin add coq 8.20.0
% make build-dep
% make -N7

All succeed.

These observations were made on commit c788b94e.

I believe that this repo is able to work on 9.0.0, though I keep getting a missing coq-lint.sh error from running make -j, so I can't fully test it to be sure.

I tried 9.0.0 earlier. make build-dep succeeded. make -N7 failed because of a wrong number of goals (I haven't saved the error message); I guess some tactics unexpectedly solved, or didn't solve subgoals.

Here's what I see on 9.0.0

% opam pin add coq 9.0.0
% make build-dep
% make -j7
File "./theories/typing/fixpoint.v", line 274, characters 8-49:
Error: Tactic failure: Incorrect number of goals (expected 1 tactic).

on masters/rusthornbelt.

Besides, master:README.md mentions 8.20.0 too.

I fixed the README to mention 8.20.1.

closed