Holomorphy

.travis.yml

@@ -21,9 +21,10 @@ 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 "cd ..; curl -LO https://github.com/math-comp/finmap/archive/1.5.0.tar.gz; tar -xvzf 1.5.0.tar.gz; cd finmap-1.5.0/; opam pin add -y -n coq-mathcomp-finmap.1.5.0 .; opam install coq-mathcomp-finmap.1.5.0; cd /home/coq/${CONTRIB}"
-- 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 coq-mathcomp-${CONTRIB}"
+- 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 coq-mathcomp-${CONTRIB}"
+- docker exec CI /bin/bash --login -c "opam install -vvv ."

_CoqProject

@@ -16,6 +16,7 @@ theories/normedtype.v
 theories/forms.v
 theories/derive.v
 theories/summability.v
+theories/cauchyetoile.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

default.nix

@@ -32,10 +32,13 @@ let
               };
             } // (cfg-fun all-pkgs);
           in {
-            # mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config {
-            #   for-coq-and-mc.${self.coq.coq-version}.${self.mathcomp.version} =
-            #     removeAttrs cfg ["mathcomp" "coq"];
-            # };
+            mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config {
+              initial = {
+                mathcomp-analysis = version:
+                  let mca = super.mathcomp-extra-config.initial.mathcomp-analysis version; in
+                  mca // { propagatedBuildInputs = mca.propagatedBuildInputs ++ [self.mathcomp-real-closed]; };
+              };
+            };
             mathcomp = if cfg?mathcomp then self.mathcomp_ cfg.mathcomp else super.mathcomp_ "1.11.0+beta1";
           } // mapAttrs
             (package: version: coqPackages.mathcomp-extra package version)

opam

@@ -22,6 +22,7 @@ depends: [
   "coq" { ((>= "8.7" & < "8.12~") | = "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: """