Set array sizes from bounds #1206
Triggered via pull request
March 12, 2025 01:02
JasonGross
Status
Failure
Total duration
4h 11m 30s
Artifacts
5
coq-debian.yml
on: pull_request
Matrix: build
Matrix: test-standalone-container
Matrix: test-standalone-host
debian-check-all
2s
Annotations
5 errors
|
debian-sid
Process completed with exit code 2.
|
|
debian-sid
Makefile.coq:818: src/Assembly/WithBedrock/SymbolicProofs.v
|
|
debian-sid
Makefile.coq:818: src/Assembly/WithBedrock/SymbolicProofs.v
|
|
debian-sid:
./src/Assembly/WithBedrock/SymbolicProofs.v#L118
The reference R_cell64 was not found in the current environment.
|
|
debian-check-all
Process completed with exit code 1.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
ExtractionHaskell-sid
|
6.29 KB |
sha256:f9e9889b967fec88d39bfbb4178f2b8dd217cf27731b219a063a672dac918908
|
|
|
ExtractionJsOfOCaml-sid
|
751 Bytes |
sha256:025d40cfd85ba26fbaef7af3aeeb9cafb95008d91672ef11c25caf1c9d80e7ec
|
|
|
ExtractionOCaml-sid
|
5.86 KB |
sha256:96af2ce46de2046ccd133fa33be664d482fabf502be9c0959822fca63d8d0703
|
|
|
generated-files-sid
|
4.87 MB |
sha256:6391b5cc2378e4cef0781a9614da3e4ab82f285ef284505c041a5a853439c864
|
|
|
timing-files-sid
|
1.84 MB |
sha256:0b29a2528b37cb5430cc049f1b5dff23dd1f5dce37f3eeb14906cc325d988fc1
|
|