Holomorphy

.travis.yml

@@ -0,0 +1,31 @@
+language: generic
+os: linux
+
+branches:
+  only:
+  - master
+
+services:
+- docker
+
+env:
+  global:
+  - NJOBS="2"
+  - CONTRIB="analysis"
+  - OPAMYES=yes
+  jobs:
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.12"
+
+install:
+- docker pull ${DOCKERIMAGE}
+- docker tag  ${DOCKERIMAGE} ci:current
+- docker run  --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
+- docker exec CI /bin/bash --login -c "opam repo add coq-released https://coq.inria.fr/opam/released"
+- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev"
+# - docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ."
+- docker exec CI /bin/bash --login -c "opam install --deps-only ."
+
+script:
+- docker exec CI /bin/bash --login -c "opam install -vvv ."

_CoqProject

@@ -24,6 +24,7 @@ theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/summability.v
+theories/holomorphy.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

config.nix

@@ -1,6 +1,6 @@
 {
   coq = "8.11";
   mathcomp = "mathcomp-1.12.0";
-  mathcomp-real-closed = "1.1.2";
+  mathcomp-real-closed = "mkerjean/master";
   mathcomp-finmap = "1.5.1";
 }

default.nix

@@ -46,7 +46,8 @@ let
                   mathcomp-analysis = {version, coqPackages} @ args:
                     let mca = mec.initial.mathcomp-analysis args; in
                     mca // (
-                      if elem version [ "master" "cauchy_etoile" "holomorphy" "numfield_topology" ]
+                      if elem version [ "master" "holomorphy" "numfield_topology" ]
+
                       then {
                         propagatedBuildInputs = mca.propagatedBuildInputs ++
                                                 [ coqPackages.mathcomp-real-closed coqPackages.hierarchy-builder ];
@@ -93,21 +94,17 @@ let
       for x in $propagatedBuildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
       echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions"
     }
-
     printEnv () {
       for x in $buildInputs; do echo $x; done
       for x in $propagatedBuildInputs; do echo $x; done
     }
-
     cachixEnv () {
       echo "Pushing environement to cachix"
       printEnv | cachix push math-comp
     }
-
     nixDefault () {
       cat $mathcompnix/default.nix
     } > default.nix
-
     updateNixPkgs (){
       HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1);
       URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz
@@ -146,4 +143,4 @@ if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
 
   propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs;
 
-}) else pkg
+}) else pkg

opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/math-comp/analysis"
+bug-reports: "https://github.com/math-comp/analysis/issues"
+dev-repo: "git+https://github.com/math-comp/analysis.git"
+license: "CECILL-C"
+authors: [
+  "Reynald Affeldt"
+  "Cyril Cohen"
+  "Assia Mahboubi"
+  "Damien Rouhling"
+  "Pierre-Yves Strub"
+]
+build: [
+  [make "INSTMODE=global" "config"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" { ((>= "8.10" & < "8.13~") | = "dev") }
+  "coq-mathcomp-field"       {(>= "1.11.0" & < "1.12~")}
+  "coq-mathcomp-finmap"      {(>= "1.5.0" & < "1.6~")}
+  "coq-mathcomp-real-closed"          {(>= "1.0.5" & < "1.1~")}
+]
+synopsis: "An analysis library for mathematical components"
+description: """
+This repository contains an experimental library for real analysis for
+the Coq proof-assistant and using the Mathematical Components library.
+
+It is inspired by the Coquelicot library.
+"""
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword: analysis"
+  "keyword: topology"
+  "keyword: real numbers"
+  "logpath: mathcomp.analysis"
+  "date:2020-08-11"
+]