diff --git a/.github/workflows/nix-action-default.yml b/.github/workflows/nix-action-default.yml new file mode 100644 index 00000000..2b834cee --- /dev/null +++ b/.github/workflows/nix-action-default.yml @@ -0,0 +1,102 @@ +jobs: + monae: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - 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 mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, math-comp + name: coq + - id: stepCheck + name: Checking presence of CI target monae + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"default\" --argstr job \"monae\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\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 "default" + --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 "default" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "mathcomp-fingroup" + - 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 "default" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "mathcomp-analysis-stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-infotheo' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "mathcomp-infotheo" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "paramcoq" + - 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 "default" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "monae" +name: Nix CI for bundle default +on: + pull_request: + paths: + - .github/workflows/nix-action-default.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-default.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix new file mode 100644 index 00000000..0615d11f --- /dev/null +++ b/.nix/config.nix @@ -0,0 +1,103 @@ +{ + ## DO NOT CHANGE THIS + format = "1.0.0"; + ## unless you made an automated or manual update + ## to another supported format. + + ## The attribute to build from the local sources, + ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` + ## Will determine the default main-job of the bundles defined below + attribute = "monae"; + + ## If you want to select a different attribute (to build from the local sources as well) + ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument + # shell-attribute = "{{nix_name}}"; + + ## Maybe the shortname of the library is different from + ## the name of the nixpkgs attribute, if so, set it here: + # pname = "{{shortname}}"; + + ## Lists the dependencies, phrased in terms of nix attributes. + ## No need to list Coq, it is already included. + ## These dependencies will systematically be added to the currently + ## known dependencies, if any more than Coq. + ## /!\ Remove this field as soon as the package is available on nixpkgs. + ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. + # buildInputs = [ ]; + + ## Indicate the relative location of your _CoqProject + ## If not specified, it defaults to "_CoqProject" + # coqproject = "_CoqProject"; + + ## select an entry to build in the following `bundles` set + ## defaults to "default" + default-bundle = "default"; + + ## write one `bundles.name` attribute set per + ## alternative configuration + ## When generating GitHub Action CI, one workflow file + ## will be created per bundle + bundles.default = { + + ## You can override Coq and other Coq coqPackages + ## through the following attribute + # coqPackages.coq.override.version = "8.11"; + + ## In some cases, light overrides are not available/enough + ## in which case you can use either + # coqPackages..overrideAttrs = o: ; + ## or a "long" overlay to put in `.nix/coq-overlays + ## you may use `nix-shell --run fetchOverlay ` + ## to automatically retrieve the one from nixpkgs + ## if it exists and is correctly named/located + + ## You can override Coq and other coqPackages + ## through the following attribute + ## If does not support light overrides, + ## you may use `overrideAttrs` or long overlays + ## located in `.nix/ocaml-overlays` + ## (there is no automation for this one) + # ocamlPackages..override.version = "x.xx"; + + ## You can also override packages from the nixpkgs toplevel + # .override.overrideAttrs = o: ; + ## Or put an overlay in `.nix/overlays` + + ## you may mark a package as a main CI job (one to take deps and + ## rev deps from) as follows + # coqPackages..main-job = true; + ## by default the current package and its shell attributes are main jobs + + ## you may mark a package as a CI job as follows + # coqPackages..job = "test"; + ## It can then built through + ## nix-build --argstr bundle "default" --arg job "test"; + ## in the absence of such a directive, the job "another-pkg" will + ## is still available, but will be automatically included in the CI + ## via the command genNixActions only if it is a dependency or a + ## reverse dependency of a job flagged as "main-job" (see above). + + ## Run on push on following branches (default [ "master" ]) + # push-branches = [ "master" "branch2" ]; + }; + + ## Cachix caches to use in CI + ## Below we list some standard ones + cachix.coq = {}; + cachix.math-comp = {}; + cachix.coq-community = {}; + + ## If you have write access to one of these caches you can + ## provide the auth token or signing key through a secret + ## variable on GitHub. Then, you should give the variable + ## name here. For instance, coq-community projects can use + ## the following line instead of the one above: + # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; + + ## Or if you have a signing key for a given Cachix cache: + # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" + + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY + ## are the names of secret variables. They are set in + ## GitHub's web interface. +} diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix new file mode 100644 index 00000000..ad3aad8c --- /dev/null +++ b/.nix/coq-nix-toolbox.nix @@ -0,0 +1 @@ +"13785ca796a883ca3f2fc1c1a1daa0ba8cea9ff2" diff --git a/.nix/coq-overlays/monae/default.nix b/.nix/coq-overlays/monae/default.nix new file mode 100644 index 00000000..6acffd9a --- /dev/null +++ b/.nix/coq-overlays/monae/default.nix @@ -0,0 +1,66 @@ +## File initially generated by createOverlay +## and then supposedly modified manually. +## Some hints for manual modifications are in the file, +## but the full doc is on nixos / nix packages website: +## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq + +{ lib, mkCoqDerivation, which, coq + ## declare extra dependencies here, to be used in propagateBuildInputs e.g. + , mathcomp, mathcomp-analysis-stdlib, mathcomp-infotheo + , paramcoq, hierarchy-builder, equations + , version ? null }: + +with lib; mkCoqDerivation { + pname = "monae"; + ## you can configure the domain, owner and repository, the default are: + # repo = "monae"; + # owner = "coq-community"; + # domain = "github.com"; + + inherit version; +## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged +## for local usage since it will be ignored locally if +## - this derivation corresponds to the main attribute, +## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + ## Add dependencies in here. In particular you can add + ## - arbitrary nix packages (you need to require them at the beginning of the file) + ## - Coq packages (require them at the beginning of the file) + ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file) + propagatedBuildInputs = [ + mathcomp.ssreflect mathcomp.fingroup mathcomp.algebra + mathcomp.solvable mathcomp-analysis-stdlib + mathcomp-infotheo + paramcoq hierarchy-builder equations + ]; ## e.g. `= [ mathcomp coq-elpi ]` + + ## Does the package contain OCaml code? + # mlPlugin = false; + + ## Give some meta data + ## This is needed for submitting the package to nixpkgs but not required for local use. + meta = { + ## Describe your package in one sentence + # description = ""; + ## Kindly ask one of these people if they want to be an official maintainer. + ## (You might also consider adding yourself to the list of maintainers) + # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ]; + ## Pick a license from + ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix + # license = licenses.mit; + }; +} diff --git a/default.nix b/default.nix new file mode 100644 index 00000000..1a24d7a1 --- /dev/null +++ b/default.nix @@ -0,0 +1,12 @@ +{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, + update-nixpkgs ? false, ci-matrix ? false, + override ? {}, ocaml-override ? {}, global-override ? {}, + bundle ? null, job ? null, inNixShell ? null, src ? ./., +}@args: +let auto = fetchGit { + url = "https://github.com/coq-community/coq-nix-toolbox.git"; + ref = "master"; + rev = import .nix/coq-nix-toolbox.nix; +}; +in +import auto ({inherit src;} // args) diff --git a/theories/lib/proba_lib.v b/theories/lib/proba_lib.v index e070d010..7a5030d6 100644 --- a/theories/lib/proba_lib.v +++ b/theories/lib/proba_lib.v @@ -5,8 +5,10 @@ Require Import Reals Lra. From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp Require boolp. From mathcomp Require Import reals mathcomp_extra Rstruct lra. +From mathcomp Require Import reals Rstruct. From infotheo Require Import ssrR realType_ext Reals_ext. From infotheo Require Import proba convex necset. +From infotheo Require Import fdist. Require Import preamble hierarchy monad_lib fail_lib. (******************************************************************************) @@ -34,10 +36,6 @@ Local Open Scope monae_scope. Local Open Scope reals_ext_scope. Local Open Scope proba_monad_scope. -From infotheo Require Import fdist. - -From mathcomp Require Import reals Rstruct. - Section convex. Variable M : probMonad R. Variable A : Type. @@ -106,7 +104,6 @@ Proof. elim: n => // n IH. by rewrite (_ : nseq _ _ = h :: nseq n.+1 h) // uniform_cons IH choicemm. Qed. -From infotheo Require Import Reals_ext. Lemma uniform_cat (M : probMonad R) (A : Type) (a : A) s t : let m := size s in let n := size t in @@ -260,7 +257,6 @@ End altprob_semilattconvtype. (* TODO(rei): incipit of section 5 of gibbonsUTP2012 on the model of MonadAltProb *) Section convexity_property. -From mathcomp.analysis Require Import Rstruct. Variables (M : altProbMonad R) (A : Type) (p q : M A).