Skip to content

Commit 2189bdd

Browse files
committed
[CI] Only run test-suite on Rocq master
1 parent 37555fb commit 2189bdd

File tree

6 files changed

+2
-1292
lines changed

6 files changed

+2
-1292
lines changed

.github/workflows/nix-action-rocq-9.0.yml

Lines changed: 0 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -7778,60 +7778,6 @@ jobs:
77787778
name: Building/fetching current CI target
77797779
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
77807780
--argstr job "stdlib-refman-html"
7781-
stdlib-test:
7782-
needs: []
7783-
runs-on: ubuntu-latest
7784-
steps:
7785-
- name: Determine which commit to initially checkout
7786-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
7787-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
7788-
}}\" >> $GITHUB_ENV\nfi\n"
7789-
- name: Git checkout
7790-
uses: actions/checkout@v4
7791-
with:
7792-
fetch-depth: 0
7793-
ref: ${{ env.target_commit }}
7794-
- name: Determine which commit to test
7795-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
7796-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
7797-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
7798-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
7799-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
7800-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
7801-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
7802-
\ fi\nfi\n"
7803-
- name: Git checkout
7804-
uses: actions/checkout@v4
7805-
with:
7806-
fetch-depth: 0
7807-
ref: ${{ env.tested_commit }}
7808-
- name: Cachix install
7809-
uses: cachix/install-nix-action@v31
7810-
with:
7811-
nix_path: nixpkgs=channel:nixpkgs-unstable
7812-
- name: Cachix setup coq
7813-
uses: cachix/cachix-action@v16
7814-
with:
7815-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
7816-
extraPullNames: coq-community, math-comp
7817-
name: coq
7818-
- id: stepGetDerivation
7819-
name: Getting derivation for current job (stdlib-test)
7820-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
7821-
\"rocq-9.0\" --argstr job \"stdlib-test\" \\\n --dry-run 2> err > out ||
7822-
(touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
7823-
derivation failed\"; exit 1; fi\n"
7824-
- id: stepCheck
7825-
name: Checking presence of CI target for current job
7826-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
7827-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
7828-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
7829-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
7830-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
7831-
- if: steps.stepCheck.outputs.status != 'fetched'
7832-
name: Building/fetching current CI target
7833-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
7834-
--argstr job "stdlib-test"
78357781
stdpp:
78367782
needs:
78377783
- coq

.nix/config.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -223,11 +223,11 @@ with builtins; with (import <nixpkgs> {}).lib;
223223
rocq-elpi.override.version = "master";
224224
rocq-elpi.override.elpi-version = "2.0.7";
225225
rocq-elpi-test.override.version = "master";
226-
stdlib-test.job = true;
227226
};
228227
in {
229228
"rocq-master" = { rocqPackages = common-bundles // {
230229
rocq-core.override.version = "master";
230+
stdlib-test.job = true;
231231
}; coqPackages = coq-common-bundles // {
232232
coq.override.version = "master";
233233
}; };

test-suite/Makefile

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -274,15 +274,6 @@ $(addsuffix .log,$(wildcard bugs/*.v success/*.v stm/*.v micromega/*.v modules/*
274274
} > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi
275275
$(HIDE)$(call REPORT_TIMER,$(patsubst %.v.log,%.chk.log,$@))
276276

277-
ROCQ_VERSION=$(shell rocq -print-version | cut -d+ -f1 | cut -d. -f1,2)
278-
279-
output_for=`\
280-
if [ -e $(1).out.$(ROCQ_VERSION) ]; then\
281-
echo $(1).out.$(ROCQ_VERSION);\
282-
else\
283-
echo $(1).out;\
284-
fi`
285-
286277
$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
287278
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
288279
$(HIDE){ \
@@ -298,7 +289,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
298289
| grep -a -v "Skipping rcfile loading" \
299290
| grep -a -v "^<W>" \
300291
> $$output; \
301-
diff -a -u --strip-trailing-cr $(call output_for,$*) $$output 2>&1; R=$$?; times; \
292+
diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
302293
if [ $$R = 0 ]; then \
303294
echo $(log_success); \
304295
echo " $<...Ok"; \

test-suite/output/Fixpoint.out.9.0

Lines changed: 0 additions & 96 deletions
This file was deleted.

0 commit comments

Comments
 (0)