From 5382aeebb01744e9d602cdc5a828a1f88e22f1bc Mon Sep 17 00:00:00 2001 From: thery Date: Thu, 19 Mar 2020 14:44:16 +0100 Subject: [PATCH 1/2] restrict libraries --- opam | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/opam b/opam index 3b13883..7cf5e51 100644 --- a/opam +++ b/opam @@ -14,10 +14,10 @@ install: [ ] remove: [make "uninstall"] depends: [ - "coq" {(>= "8.9")} - "coq-mathcomp-ssreflect" { (>= "1.7") } - "coq-mathcomp-algebra" {>= "1.7"} - "coq-coquelicot" {(>= "3.0")} + "coq" {(>= "8.9" & < "8.10~")} + "coq-mathcomp-ssreflect" { (>= "1.7" & < "1.8~") } + "coq-mathcomp-algebra" {>= "1.7" & < "1.8~"} + "coq-coquelicot" {(>= "3.0" & < "3.1~")} ] tags: [ ] From d89f6dd83d045c7fe0fa8709dc139e56cbd30a01 Mon Sep 17 00:00:00 2001 From: thery Date: Mon, 23 Mar 2020 14:11:51 +0100 Subject: [PATCH 2/2] change makefile to avoid sandboxing --- Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 9d0fc9e..81686bf 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ SUBDIRS := mf rlzrs metric incone all: - cd mf; make; make install; - cd rlzrs; make; make install; - cd metric; make; make install; - cd incone; make; make install + cd mf; make; + cd rlzrs; make COQEXTRAFLAGS="-R ../mf mf"; + cd metric;make COQEXTRAFLAGS="-R ../mf mf -R ../rlzrs rlzrs"; + cd incone;make COQEXTRAFLAGS="-R ../mf mf -R ../rlzrs rlzrs -R ../metric metric" clean: cd mf; make clean;