Skip to content

adapt to coq/coq#15948 #293

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 51 commits into from
Apr 28, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
f1c340d
HB.structure: refresh universes in coercions (fix #248)
gares Jul 23, 2021
061ab25
fix nix
gares Jul 23, 2021
d617855
Merge pull request #262 from math-comp/fix-248
gares Jul 24, 2021
638fc6f
wip
CohenCyril May 10, 2021
cb19e48
skipping
CohenCyril May 10, 2021
6e4be80
optim successfull
CohenCyril May 10, 2021
c537978
remove dead code
gares Jul 26, 2021
230fae1
rewrite structure-instance->mixin-srcs (fix #257)
gares Jul 26, 2021
ecc19dc
nah
gares Jul 26, 2021
27567c4
nix leftover
gares Jul 27, 2021
13d6daf
more comments
gares Jul 27, 2021
a0a22a6
cleanup
gares Jul 27, 2021
f812842
improve doc, avoid corner case
gares Jul 27, 2021
474a56e
Merge pull request #242 from math-comp/optim-instances
gares Jul 27, 2021
1461a12
improve makefile + test
gares Sep 1, 2021
951f295
#[hnf]
gares Aug 31, 2021
e53d0a0
Merge pull request #264 from math-comp/hnf
gares Sep 1, 2021
40624b9
document #[hnf]
gares Sep 24, 2021
f6fec96
Merge pull request #266 from math-comp/improve-doc-hnf
gares Sep 24, 2021
fc644ba
Update Changelog.md
gares Sep 24, 2021
e798ab4
Merge pull request #267 from math-comp/update-changelog
gares Sep 24, 2021
5988d20
Update config.nix
gares Sep 24, 2021
33bf9c4
Merge pull request #268 from math-comp/fix-ci
gares Sep 24, 2021
e3f3f52
Update Changelog.md
gares Sep 24, 2021
952607d
Merge pull request #269 from math-comp/close-changelog
gares Sep 24, 2021
992c3f5
Update coq-hierarchy-builder-shim.opam
gares Sep 25, 2021
6953bee
test 8.14
gares Oct 21, 2021
eda535d
Fix test suite for 8.14
gares Oct 21, 2021
f65d7c5
Merge pull request #272 from math-comp/ci8.14
gares Oct 22, 2021
0ddf09b
One more coq version is supported
CohenCyril Oct 29, 2021
e881554
nix toolbox update
CohenCyril Oct 29, 2021
ad382f6
Merge pull request #273 from math-comp/coq-8.14
CohenCyril Nov 2, 2021
e288c75
complete CI mathcomp on HB
CohenCyril Nov 8, 2021
e8eabc6
Revert "complete CI mathcomp on HB"
CohenCyril Nov 8, 2021
65f2384
complete CI mathcomp on HB
CohenCyril Nov 8, 2021
2fa17b7
Merge pull request #275 from math-comp/CImcHB
CohenCyril Nov 9, 2021
d7300b6
Add cachix tokens and update nix actions
CohenCyril Nov 30, 2021
d749055
Merge pull request #278 from math-comp/cachix
CohenCyril Nov 30, 2021
073e684
do not unfold letins in instances
gares Nov 10, 2021
4d2398f
oothm -> HB
gares Nov 10, 2021
f11da02
Update .nix/config.nix
CohenCyril Nov 30, 2021
ff2d94f
fix typo in hb.ml (fix #279)
gares Dec 3, 2021
a06930d
Merge pull request #276 from math-comp/faster-hb-pack
CohenCyril Dec 15, 2021
14dfa74
Merge pull request #270 from math-comp/fix-opam
gares Dec 15, 2021
ffb8037
[ci] docker on 8.15
gares Jan 9, 2022
192dcc2
[tests] fix 8.15
gares Jan 9, 2022
9614134
Merge pull request #282 from math-comp/ci-8.15
gares Jan 9, 2022
23aa065
update changelog
gares Jan 9, 2022
cbb3df1
HB arguments are raw
gares Apr 27, 2022
b24760c
Merge branch 'master' into bump-elpi
gares Apr 28, 2022
379dc28
compat with coq-elpi 1.14
gares Apr 7, 2022
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ jobs:
matrix:
coq_version:
- '8.13'
- '8.14'
- '8.15'
ocaml_version:
- '4.07-flambda'
steps:
Expand All @@ -38,7 +40,7 @@ jobs:
- uses: coq-community/docker-coq-action@v1
with:
opam_file: './coq-hierarchy-builder.opam'
coq_version: '8.13'
coq_version: '8.14'
ocaml_version: '4.07-flambda'
script: |
mkdir /home/coq/workspace
Expand Down
315 changes: 315 additions & 0 deletions .github/workflows/nix-action-coq-8.13.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,315 @@
jobs:
coq:
needs: []
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target coq
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
\ \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
graph-theory:
needs:
- coq
- hierarchy-builder
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target graph-theory
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"graph-theory\" \\\n --dry-run 2>&1\
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-algebra'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-algebra"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-finmap'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-finmap"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: hierarchy-builder'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "hierarchy-builder"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "graph-theory"
hierarchy-builder:
needs:
- coq
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target hierarchy-builder
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"hierarchy-builder\" \\\n --dry-run\
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq-elpi'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq-elpi"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "hierarchy-builder"
mathcomp-analysis:
needs:
- coq
- hierarchy-builder
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target mathcomp-analysis
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-ssreflect"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-field'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-field"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-finmap'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-finmap"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-bigenough'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-bigenough"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: mathcomp-real-closed'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-real-closed"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: hierarchy-builder'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "hierarchy-builder"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-analysis"
mathcomp-single:
needs:
- coq
- hierarchy-builder
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target mathcomp-single
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"mathcomp-single\" \\\n --dry-run 2>&1\
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq-elpi'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq-elpi"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: hierarchy-builder'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "hierarchy-builder"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-single"
mathcomp-single-planB-src:
needs:
- coq
- hierarchy-builder
runs-on: ubuntu-latest
steps:
- name: Determine which commit to test
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
\ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\
\ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\
\ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
- name: Git checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
ref: ${{ env.tested_commit }}
- name: Cachix install
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixpkgs-unstable
- name: Cachix setup math-comp
uses: cachix/cachix-action@v10
with:
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
extraPullNames: coq, coq-community
name: math-comp
- id: stepCheck
name: Checking presence of CI target mathcomp-single-planB-src
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
\ bundle \"coq-8.13\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: coq-elpi'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "coq-elpi"
- if: steps.stepCheck.outputs.status == 'built'
name: 'Building/fetching previous CI target: hierarchy-builder'
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "hierarchy-builder"
- if: steps.stepCheck.outputs.status == 'built'
name: Building/fetching current CI target
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
--argstr job "mathcomp-single-planB-src"
name: Nix CI for bundle coq-8.13
'on':
pull_request:
paths:
- .github/workflows/**
pull_request_target:
types:
- opened
- synchronize
- reopened
push:
branches:
- master
Loading