libre-chip/fayalite
3
0
Fork 3
Code Issues 1 Pull requests 1 Projects Releases Packages Wiki Activity Actions

Run Rocq tests. #64

Open
cesar wants to merge 1 commit from cesar/fayalite:run-rocq-tests into master
pull from: cesar/fayalite:run-rocq-tests
merge into: libre-chip:master
Conversation 1 Commits 1 Files changed 5 +46 -1
cesar commented 2026-02-14 22:05:52 +00:00
Owner
Copy link
No description provided.
cesar added 1 commit 2026-02-14 22:05:52 +00:00
Run Rocq tests.
Some checks failed
/ test (pull_request) Failing after 34s
Details
845813d4bb
cesar force-pushed run-rocq-tests from 845813d4bb to 226bfe98d0 2026-02-14 22:16:14 +00:00 Compare
cesar commented 2026-02-15 11:56:03 +00:00
Author
Owner
Copy link

I really don't understand why the CI runner doesn't find rocq.

make: Entering directory '/workspace/libre-chip/fayalite/rocq-demo'
rocq makefile -f _CoqProject -o CoqMakefile
make: rocq: No such file or directory
make: *** [Makefile:18: CoqMakefile] Error 127
make: Leaving directory '/workspace/libre-chip/fayalite/rocq-demo'

I tried locally:

$ docker pull git.libre-chip.org/libre-chip/fayalite-deps:latest
...
$ docker images
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
REPOSITORY                                   TAG         IMAGE ID      CREATED     SIZE
git.libre-chip.org/libre-chip/fayalite-deps  latest      a345fbffea98  6 days ago  7.49 GB

$ docker run --rm a345fbffea98 rocq -v
Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg.
The Rocq Prover, version 9.0.1
compiled with OCaml 4.13.1
I really don't understand why the CI runner doesn't find rocq. ``` make: Entering directory '/workspace/libre-chip/fayalite/rocq-demo' rocq makefile -f _CoqProject -o CoqMakefile make: rocq: No such file or directory make: *** [Makefile:18: CoqMakefile] Error 127 make: Leaving directory '/workspace/libre-chip/fayalite/rocq-demo' ``` I tried locally: ``` $ docker pull git.libre-chip.org/libre-chip/fayalite-deps:latest ... $ docker images Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg. REPOSITORY TAG IMAGE ID CREATED SIZE git.libre-chip.org/libre-chip/fayalite-deps latest a345fbffea98 6 days ago 7.49 GB $ docker run --rm a345fbffea98 rocq -v Emulate Docker CLI using podman. Create /etc/containers/nodocker to quiet msg. The Rocq Prover, version 9.0.1 compiled with OCaml 4.13.1 ```
Some checks failed
/ test (pull_request) Failing after 35s
Required
Details
Some required checks were not successful.
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u run-rocq-tests:cesar-run-rocq-tests
git checkout cesar-run-rocq-tests
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: libre-chip/fayalite#64
No description provided.
Delete branch "cesar/fayalite:run-rocq-tests"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?