Skip to content

Commit 7acb6d7

Browse files
mattam82mattam82
authored
Merge pull request #749 from MetaCoq/8.15-cherry-picks
8.15 cherry picks
2 parents 64bdee8 + dbb6943 commit 7acb6d7

File tree

146 files changed

+5140
-1309
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

146 files changed

+5140
-1309
lines changed

‎.github/workflows/nix-action-default-macos.yml‎

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
env:
2+
BUNDLE: "coq-8.15"
3+
4+
jobs:
5+
coq:
6+
needs: []
7+
runs-on: macos-latest
8+
steps:
9+
- name: Determine which commit to test
10+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
11+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
12+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
13+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
14+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
15+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
16+
- name: Git checkout
17+
uses: actions/checkout@v2
18+
with:
19+
fetch-depth: 0
20+
ref: ${{ env.tested_commit }}
21+
- name: Cachix install
22+
uses: cachix/install-nix-action@v16
23+
with:
24+
nix_path: nixpkgs=channel:nixpkgs-unstable
25+
- name: Cachix setup metacoq
26+
uses: cachix/cachix-action@v10
27+
with:
28+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
29+
extraPullNames: coq, coq-community
30+
name: metacoq
31+
- id: stepCheck
32+
name: Checking presence of CI target coq
33+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
34+
\ bundle \"$BUNDLE\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
35+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
36+
\ \"built:\" | sed \"s/.*/built/\")\n"
37+
- if: steps.stepCheck.outputs.status == 'built'
38+
name: Building/fetching current CI target
39+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
40+
--argstr job "coq"
41+
equations:
42+
needs:
43+
- coq
44+
runs-on: macos-latest
45+
steps:
46+
- name: Determine which commit to test
47+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
48+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
49+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
50+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
51+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
52+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
53+
- name: Git checkout
54+
uses: actions/checkout@v2
55+
with:
56+
fetch-depth: 0
57+
ref: ${{ env.tested_commit }}
58+
- name: Cachix install
59+
uses: cachix/install-nix-action@v16
60+
with:
61+
nix_path: nixpkgs=channel:nixpkgs-unstable
62+
- name: Cachix setup metacoq
63+
uses: cachix/cachix-action@v10
64+
with:
65+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
66+
extraPullNames: coq, coq-community
67+
name: metacoq
68+
- id: stepCheck
69+
name: Checking presence of CI target equations
70+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
71+
\ bundle \"$BUNDLE\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\
72+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
73+
\ \"built:\" | sed \"s/.*/built/\")\n"
74+
- if: steps.stepCheck.outputs.status == 'built'
75+
name: 'Building/fetching previous CI target: coq'
76+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
77+
--argstr job "coq"
78+
- if: steps.stepCheck.outputs.status == 'built'
79+
name: Building/fetching current CI target
80+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
81+
--argstr job "equations"
82+
metacoq:
83+
needs:
84+
- coq
85+
- equations
86+
runs-on: macos-latest
87+
steps:
88+
- name: Determine which commit to test
89+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
90+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
91+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
92+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
93+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
94+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
95+
- name: Git checkout
96+
uses: actions/checkout@v2
97+
with:
98+
fetch-depth: 0
99+
ref: ${{ env.tested_commit }}
100+
- name: Cachix install
101+
uses: cachix/install-nix-action@v16
102+
with:
103+
nix_path: nixpkgs=channel:nixpkgs-unstable
104+
- name: Cachix setup metacoq
105+
uses: cachix/cachix-action@v10
106+
with:
107+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
108+
extraPullNames: coq, coq-community
109+
name: metacoq
110+
- id: stepCheck
111+
name: Checking presence of CI target metacoq
112+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
113+
\ bundle \"$BUNDLE\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\
114+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
115+
\ \"built:\" | sed \"s/.*/built/\")\n"
116+
- if: steps.stepCheck.outputs.status == 'built'
117+
name: 'Building/fetching previous CI target: coq'
118+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
119+
--argstr job "coq"
120+
- if: steps.stepCheck.outputs.status == 'built'
121+
name: 'Building/fetching previous CI target: equations'
122+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
123+
--argstr job "equations"
124+
- if: steps.stepCheck.outputs.status == 'built'
125+
name: 'Building/fetching previous CI target: metacoq-template-coq'
126+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
127+
--argstr job "metacoq-template-coq"
128+
- if: steps.stepCheck.outputs.status == 'built'
129+
name: 'Building/fetching previous CI target: metacoq-pcuic'
130+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
131+
--argstr job "metacoq-pcuic"
132+
- if: steps.stepCheck.outputs.status == 'built'
133+
name: 'Building/fetching previous CI target: metacoq-safechecker'
134+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
135+
--argstr job "metacoq-safechecker"
136+
- if: steps.stepCheck.outputs.status == 'built'
137+
name: 'Building/fetching previous CI target: metacoq-erasure'
138+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
139+
--argstr job "metacoq-erasure"
140+
- if: steps.stepCheck.outputs.status == 'built'
141+
name: Building/fetching current CI target
142+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
143+
--argstr job "metacoq"
144+
name: Nix CI
145+
'on':
146+
pull_request:
147+
paths:
148+
- .github/workflows/**
149+
pull_request_target:
150+
types:
151+
- opened
152+
- synchronize
153+
- reopened
154+
push:
155+
branches:
156+
- master

‎.github/workflows/nix-action-default-ubuntu.yml‎

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
env:
2+
BUNDLE: coq-8.15
3+
4+
jobs:
5+
coq:
6+
needs: []
7+
runs-on: ubuntu-latest
8+
steps:
9+
- name: Determine which commit to test
10+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
11+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
12+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
13+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
14+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
15+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
16+
- name: Git checkout
17+
uses: actions/checkout@v2
18+
with:
19+
fetch-depth: 0
20+
ref: ${{ env.tested_commit }}
21+
- name: Cachix install
22+
uses: cachix/install-nix-action@v16
23+
with:
24+
nix_path: nixpkgs=channel:nixpkgs-unstable
25+
- name: Cachix setup metacoq
26+
uses: cachix/cachix-action@v10
27+
with:
28+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
29+
extraPullNames: coq, coq-community
30+
name: metacoq
31+
- id: stepCheck
32+
name: Checking presence of CI target coq
33+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
34+
\ bundle \"$BUNDLE\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
35+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
36+
\ \"built:\" | sed \"s/.*/built/\")\n"
37+
- if: steps.stepCheck.outputs.status == 'built'
38+
name: Building/fetching current CI target
39+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
40+
--argstr job "coq"
41+
equations:
42+
needs:
43+
- coq
44+
runs-on: ubuntu-latest
45+
steps:
46+
- name: Determine which commit to test
47+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
48+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
49+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
50+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
51+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
52+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
53+
- name: Git checkout
54+
uses: actions/checkout@v2
55+
with:
56+
fetch-depth: 0
57+
ref: ${{ env.tested_commit }}
58+
- name: Cachix install
59+
uses: cachix/install-nix-action@v16
60+
with:
61+
nix_path: nixpkgs=channel:nixpkgs-unstable
62+
- name: Cachix setup metacoq
63+
uses: cachix/cachix-action@v10
64+
with:
65+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
66+
extraPullNames: coq, coq-community
67+
name: metacoq
68+
- id: stepCheck
69+
name: Checking presence of CI target equations
70+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
71+
\ bundle \"$BUNDLE\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\
72+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
73+
\ \"built:\" | sed \"s/.*/built/\")\n"
74+
- if: steps.stepCheck.outputs.status == 'built'
75+
name: 'Building/fetching previous CI target: coq'
76+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
77+
--argstr job "coq"
78+
- if: steps.stepCheck.outputs.status == 'built'
79+
name: Building/fetching current CI target
80+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
81+
--argstr job "equations"
82+
metacoq:
83+
needs:
84+
- coq
85+
- equations
86+
runs-on: ubuntu-latest
87+
steps:
88+
- name: Determine which commit to test
89+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
90+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
91+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
92+
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
93+
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
94+
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
95+
- name: Git checkout
96+
uses: actions/checkout@v2
97+
with:
98+
fetch-depth: 0
99+
ref: ${{ env.tested_commit }}
100+
- name: Cachix install
101+
uses: cachix/install-nix-action@v16
102+
with:
103+
nix_path: nixpkgs=channel:nixpkgs-unstable
104+
- name: Cachix setup metacoq
105+
uses: cachix/cachix-action@v10
106+
with:
107+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
108+
extraPullNames: coq, coq-community
109+
name: metacoq
110+
- id: stepCheck
111+
name: Checking presence of CI target metacoq
112+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
113+
\ bundle \"$BUNDLE\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\
114+
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
115+
\ \"built:\" | sed \"s/.*/built/\")\n"
116+
- if: steps.stepCheck.outputs.status == 'built'
117+
name: 'Building/fetching previous CI target: coq'
118+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
119+
--argstr job "coq"
120+
- if: steps.stepCheck.outputs.status == 'built'
121+
name: 'Building/fetching previous CI target: equations'
122+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
123+
--argstr job "equations"
124+
- if: steps.stepCheck.outputs.status == 'built'
125+
name: 'Building/fetching previous CI target: metacoq-template-coq'
126+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
127+
--argstr job "metacoq-template-coq"
128+
- if: steps.stepCheck.outputs.status == 'built'
129+
name: 'Building/fetching previous CI target: metacoq-pcuic'
130+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
131+
--argstr job "metacoq-pcuic"
132+
- if: steps.stepCheck.outputs.status == 'built'
133+
name: 'Building/fetching previous CI target: metacoq-safechecker'
134+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
135+
--argstr job "metacoq-safechecker"
136+
- if: steps.stepCheck.outputs.status == 'built'
137+
name: 'Building/fetching previous CI target: metacoq-erasure'
138+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
139+
--argstr job "metacoq-erasure"
140+
- if: steps.stepCheck.outputs.status == 'built'
141+
name: Building/fetching current CI target
142+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "$BUNDLE"
143+
--argstr job "metacoq"
144+
name: Nix CI
145+
'on':
146+
pull_request:
147+
paths:
148+
- .github/workflows/**
149+
pull_request_target:
150+
types:
151+
- opened
152+
- synchronize
153+
- reopened
154+
push:
155+
branches:
156+
- master

‎.nix/cachedMake.sh‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
#! /usr/bin/bash
2+
3+
# USAGE: To be run from the top directory of metacoq
4+
5+
# This whole file is a hack around coq-nix-toolbox to manage the
6+
# structure of metacoq directories
7+
8+
export currentDir=$PWD
9+
export configDir=$currentDir/.nix
10+
11+
#There should be a way to ask nix directly
12+
coq_version='8.14'
13+
14+
my-nix-build-with-target (){
15+
target=$1
16+
shift
17+
env -i PATH=$PATH NIX_PATH=$NIX_PATH nix-build -A $target \
18+
--argstr bundle "$selectedBundle" --no-out-link\
19+
--option narinfo-cache-negative-ttl 0 $*
20+
}
21+
22+
my-cachedMake (){
23+
cproj=$currentDir/$coqproject
24+
cprojDir=$(dirname $cproj)
25+
nb_dry_run=$(my-nix-build-with-target $1 --dry-run 2>&1 > /dev/null)
26+
if echo $nb_dry_run | grep -q "built:"; then
27+
echo "The compilation result is not in cache."
28+
echo "Either it is not in cache (yet) or your must check your cachix configuration."
29+
kill -INT $$
30+
else
31+
build=$(my-nix-build-with-target $1)
32+
realpath=$2
33+
namespace=$3
34+
logpath=${namespace/.//}
35+
vopath="$build/lib/coq/$coq_version/user-contrib/$logpath"
36+
dest=$cprojDir/$realpath
37+
if [[ -d $vopath ]]
38+
then echo "Compiling/Fetching and copying vo from $vopath to $realpath"
39+
cp -nr --no-preserve=mode,ownership $vopath/* $dest
40+
else echo "Error: cannot find compiled $logpath, check your .nix/config.nix"
41+
fi
42+
fi
43+
}
44+
45+
my-cachedMake 'template-coq' 'template-coq/theories' 'MetaCoq.Template'
46+
my-cachedMake 'pcuic' 'pcuic/theories' 'MetaCoq.PCUIC'
47+
my-cachedMake 'safechecker' 'safechecker/theories' 'MetaCoq.SafeChecker'
48+
my-cachedMake 'erasure' 'erasure/theories' 'MetaCoq.Erasure'
49+
50+
unset -f my-nix-build-with-target
51+
unset -f my-cachedMake

0 commit comments

Comments
 (0)