kami

kami copied to clipboard

Make command fails with Coq 8.11.1

2

Make fails when run with Coq 8.11.1. The output is as follows: `$make` ``` Generating Makefile make -f Makefile.coq.all make[1]: Entering directory '/home/vaishnavi/kami' COQDEP VFILES COQC Kami/Lib/StringStringAsOT.v File "./Kami/Lib/StringStringAsOT.v", line...

vaishnavi08

Bluespec 2023.01

1

`make` succeeded, I was able to generate the .bsv from Target.ml. Some of the bluespec includes seem to no longer exist compared to 2014.01. Any hints on what to do?...

hchenji

Adapt to https://github.com/rocq-prover/rocq/pull/17876 Sorry, apparently my previous attempt was incomplete. At least this time CI on the upstream PR seems to confirm we are good.

proux01

I'm getting errors saying the server is unreachable.

dead-claudia