From 89897f111036ca5b120fe4522e94425f59ae2dd2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Nov 2022 15:02:40 +0100 Subject: [PATCH] math-comp-school-2022 --- .github/workflows/macos.yml | 10 +-- .github/workflows/ubuntu.yml | 13 +-- .github/workflows/ubuntu_dev.yml | 79 ------------------ .github/workflows/windows.yml | 12 +-- .../coq-mathcomp-algebra.2.0.0+alpha1/opam | 26 ++++++ .../coq-mathcomp-character.2.0.0+alpha1/opam | 24 ++++++ .../coq-mathcomp-field.2.0.0+alpha1/opam | 24 ++++++ .../coq-mathcomp-fingroup.2.0.0+alpha1/opam | 24 ++++++ .../coq-mathcomp-solvable.2.0.0+alpha1/opam | 24 ++++++ .../coq-mathcomp-ssreflect.2.0.0+alpha1/opam | 31 +++++++ .../package-pick-math-comp-school-2022 | 82 +++++++++++++++++++ 11 files changed, 244 insertions(+), 105 deletions(-) delete mode 100644 .github/workflows/ubuntu_dev.yml create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.0.0+alpha1/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.0.0+alpha1/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.0.0+alpha1/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.0.0+alpha1/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.0.0+alpha1/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.0.0+alpha1/opam create mode 100644 package_picks/package-pick-math-comp-school-2022 diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml index 884c7b5681..e84831150d 100644 --- a/.github/workflows/macos.yml +++ b/.github/workflows/macos.yml @@ -12,9 +12,7 @@ name: Macos on: push: branches: - - 2021.02 - - 2021.09 - - main + - math-comp-school-2022 pull_request: branches: - '**' @@ -48,8 +46,7 @@ jobs: fail-fast: false matrix: variant: - - '8.16~2022.09~beta1' - - '8.15~2022.04' + - 'math-comp-school-2022' steps: - name: Git checkout @@ -124,8 +121,7 @@ jobs: fail-fast: false matrix: variant: - - '8.16~2022.09~beta1' - - '8.15~2022.04' + - 'math-comp-school-2022' steps: - name: Install bash diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml index c3a915b8b2..d222fb296f 100644 --- a/.github/workflows/ubuntu.yml +++ b/.github/workflows/ubuntu.yml @@ -12,9 +12,7 @@ name: Ubuntu on: push: branches: - - 2021.02 - - 2021.09 - - main + - math-comp-school-2022 pull_request: branches: - '**' @@ -39,7 +37,7 @@ on: env: PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y COQREGTESTING: y - SNAP_PICK: 8.16~2022.09~beta1 + SNAP_PICK: math-comp-school-2022 ############################################################################### # Ubuntu @@ -57,12 +55,7 @@ jobs: matrix: variant: # This should contain all picks introduced in the current release + all original picks of all Coq versions - - '8.16~2022.09~beta1' - - '8.15~2022.09~beta1' - - '8.15~2022.04' - - '8.14~2022.01' - - '8.13~2021.02' - - '8.12' + - 'math-comp-school-2022' steps: - name: Git checkout diff --git a/.github/workflows/ubuntu_dev.yml b/.github/workflows/ubuntu_dev.yml deleted file mode 100644 index b279d83560..0000000000 --- a/.github/workflows/ubuntu_dev.yml +++ /dev/null @@ -1,79 +0,0 @@ -# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions -# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners -# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob - -name: Ubuntu_dev - -############################################################################### -# Schedule: -# - daily -############################################################################### -on: - schedule: - - cron: "0 0 * * *" - workflow_dispatch: - inputs: - platform: - description: 'Arguments for the platform script:' - required: true - default: '-extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y' - -############################################################################### -# Platform script options shared among all jobs -############################################################################### -env: - PLATFORM: -extent=x -parallel=p -jobs=2 -large=i -compcert=y -unimath=n -set-switch=y - COQREGTESTING: y - -############################################################################### -# Ubuntu -# -# CAVEATS: -# - you need bubblewrap or the script fails -# - build-essential pulls in the C toolchain -############################################################################### -jobs: - Ubuntu_platform: - name: Ubuntu - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - variant: - - 'dev' - - steps: - - name: Git checkout - uses: actions/checkout@v2 - - - name: Set PLATFORM - if: ${{ github.event.inputs.platform != '' }} - run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV - - - name: Install bubblewrap and build-essential - run: | - sudo apt-get update - sudo apt-get install bubblewrap build-essential - - - name: Run common platform script - shell: bash - run: ./coq_platform_make.sh -packages=${{matrix.variant}} $PLATFORM -dumplogs - - - name: Create smoke test kit - shell: bash - run: | - eval $(opam env) - shell_scripts/create_smoke_test_kit.sh - - - name: 'Run Linux smoke test kit' - shell: bash - run: | - eval $(opam env) - smoke-test-kit/run-smoke-test.sh - - - name: 'Upload smoke test kit' - uses: actions/upload-artifact@v2 - with: - name: 'Smoke Test Kit ${{matrix.variant}}' - path: smoke-test-kit - retention-days: 5 diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml index b161bfb556..4331c3bc41 100644 --- a/.github/workflows/windows.yml +++ b/.github/workflows/windows.yml @@ -12,9 +12,7 @@ name: Windows on: push: branches: - - 2021.02 - - 2021.09 - - main + - math-comp-school-2022 pull_request: branches: - '**' @@ -50,12 +48,10 @@ jobs: fail-fast: false matrix: architecture: - - '32' - '64' variant: # Keep this in sync with the Smoke test below - - '8.16~2022.09~beta1' - - '8.15~2022.04' + - 'math-comp-school-2022' steps: - name: Set git to use LF @@ -104,11 +100,9 @@ jobs: fail-fast: false matrix: architecture: - - '32' - '64' variant: - - '8.16~2022.09~beta1' - - '8.15~2022.04' + - 'math-comp-school-2022' steps: - name: 'Download Artifact' diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.0.0+alpha1/opam new file mode 100644 index 0000000000..d7ffc40204 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.0.0+alpha1/opam @@ -0,0 +1,26 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/algebra" "install" ] +depends: [ "coq-mathcomp-fingroup" { = version } ] + +tags: [ "keyword:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.algebra" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on Algebra" +description: """ +This library contains definitions and theorems about discrete +(i.e. with decidable equality) algebraic structures : ring, fields, +ordered fields, real fields, modules, algebras, integers, rational +numbers, polynomials, matrices, vector spaces... +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.0.0+alpha1/opam new file mode 100644 index 0000000000..9cacc1c006 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.0.0+alpha1/opam @@ -0,0 +1,24 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/character" "install" ] +depends: [ "coq-mathcomp-field" { = version } ] + +tags: [ "keyword:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.character" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on character theory" +description:""" +This library contains definitions and theorems about group +representations, characters and class functions. +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.0.0+alpha1/opam new file mode 100644 index 0000000000..a570dceabc --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.0.0+alpha1/opam @@ -0,0 +1,24 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/field" "install" ] +depends: [ "coq-mathcomp-solvable" { = version } ] + +tags: [ "keyword:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.field" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on Fields" +description:""" +This library contains definitions and theorems about field extensions, +galois theory, algebraic numbers, cyclotomic polynomials... +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.0.0+alpha1/opam new file mode 100644 index 0000000000..597646c9db --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.0.0+alpha1/opam @@ -0,0 +1,24 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/fingroup" "install" ] +depends: [ "coq-mathcomp-ssreflect" { = version } ] + +tags: [ "keyword:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.fingroup" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on finite groups" +description: """ +This library contains definitions and theorems about finite groups, +group quotients, group morphisms, group presentation, group action... +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.0.0+alpha1/opam new file mode 100644 index 0000000000..a11b026702 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.0.0+alpha1/opam @@ -0,0 +1,24 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/solvable" "install" ] +depends: [ "coq-mathcomp-algebra" { = version } ] + +tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.solvable" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on finite groups (II)" + +description:""" +This library contains more definitions and theorems about finite groups. +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.0.0+alpha1/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.0.0+alpha1/opam new file mode 100644 index 0000000000..b88c4885d2 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.0.0+alpha1/opam @@ -0,0 +1,31 @@ +opam-version: "2.0" +version: "dev" +maintainer: "Mathematical Components " + +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" +license: "CECILL-B" + +build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/ssreflect" "install" ] +depends: [ + "coq" { ((>= "8.13" & < "8.17~") | (= "dev"))} + "coq-hierarchy-builder" { >= "1.4.0"} +] + +tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Small Scale Reflection" +description: """ +This library includes the small scale reflection proof language +extension and the minimal set of libraries to take advantage of it. +This includes libraries on lists (seq), boolean and boolean +predicates, natural numbers and types with decidable equality, +finite types, finite sets, finite functions, finite graphs, basic arithmetics +and prime numbers, big operators +""" +url { + src: "https://github.com/math-comp/math-comp/zipball/hierarchy-builder" +} \ No newline at end of file diff --git a/package_picks/package-pick-math-comp-school-2022 b/package_picks/package-pick-math-comp-school-2022 new file mode 100644 index 0000000000..fadd5dd006 --- /dev/null +++ b/package_picks/package-pick-math-comp-school-2022 @@ -0,0 +1,82 @@ +#!/usr/bin/env bash + +###################### COPYRIGHT/COPYLEFT ###################### + +# (C) 2020..2022 Michael Soegtrop + +# Released to the public under the +# Creative Commons CC0 1.0 Universal License +# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt + +###################### CONTROL VARIABLES ##################### + +# The two lines below are used by the package selection script +COQ_PLATFORM_VERSION_TITLE="Coq 8.16.0 (released Sep 2022) with a package pick for the 2022 Math Comp school." +COQ_PLATFORM_VERSION_SORTORDER=9000 + +# The package list name is the final part of the opam switch name. +# It is usually either empty ot starts with ~. +# It might also be used for installer package names, but with ~ replaced by _ +# It is also used for version specific file selections in the smoke test kit. +COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~math-comp-school-2022' + +# The corresponding Coq development branch and tag +COQ_PLATFORM_COQ_BRANCH='v8.16' +COQ_PLATFORM_COQ_TAG='8.16.0' + +# This controls if opam repositories for development packages are selected +COQ_PLATFORM_USE_DEV_REPOSITORY='N' + +# This extended descriptions is used for readme files +COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2022.09.0 includes Coq 8.16.0 from Sep 2022. ' +COQ_PLATFORM_VERSION_DESCRIPTION+='This is beta release with complete package pick and intended for package maintainers and early adopters. ' + +# The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way) +COQ_PLATFORM_OCAML_VERSION='4.13.1' + +###################### PACKAGE SELECTION ##################### + +PACKAGES="" + +# - Comment out packages you do not want. +# - Packages which take a long time to build should be given last. +# There is some evidence that they are built early then. +# - Versions ending with ~flex are identical to the opam package without the +# ~flex extension, except that version restrictions have been relaxed. +# - The picking tracker issue is https://github.com/coq/platform/issues/193 + +########## BASE PACKAGES ########## + +# Coq needs a patched ocamlfind to be relocatable by installers +PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.5~relocatable" +# The Coq compiler coqc and the Coq standard library +PACKAGES="${PACKAGES} PIN.coq.8.16.0" +# Since dune does support Coq, it is explicitly selected +PACKAGES="${PACKAGES} dune.3.4.1" +PACKAGES="${PACKAGES} dune-configurator.3.4.1" + +########## IDE PACKAGES ########## + +# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]] +then +PACKAGES="${PACKAGES} coqide.8.16.0" +fi + +########## "FULL" COQ PLATFORM PACKAGES ########## + +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[fFxX] ]] +then + + PACKAGES="${PACKAGES} elpi.1.16.5 coq-elpi.1.15.6" + PACKAGES="${PACKAGES} coq-hierarchy-builder.1.4.0" + PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.0.0+alpha1" + PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.0.0+alpha1" + PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.0.0+alpha1" + PACKAGES="${PACKAGES} coq-mathcomp-solvable.2.0.0+alpha1" + PACKAGES="${PACKAGES} coq-mathcomp-field.2.0.0+alpha1" + PACKAGES="${PACKAGES} coq-mathcomp-character.2.0.0+alpha1" + +# PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.0.0" + +fi \ No newline at end of file