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

Run Rocq tests. #64

Merged
cesar merged 1 commit from cesar/fayalite:run-rocq-tests into master 2026-03-31 00:22:46 +00:00
Conversation 2 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 ```
programmerjake approved these changes 2026-03-18 03:59:15 +00:00
programmerjake left a comment
Owner
Copy link

once you rebase this feel free to merge

once you rebase this feel free to merge
cesar force-pushed run-rocq-tests from 226bfe98d0 to 8cff3687f7 2026-03-30 22:39:04 +00:00 Compare
cesar merged commit 8cff3687f7 into master 2026-03-31 00:22:46 +00:00
Sign in to join this conversation.
Reviewers
No reviewers
programmerjake
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
2 participants
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?