From 332d85dc6c69fbcc2aae7b9d4af975fb43769b05 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 23:43:09 -0400 Subject: Add coq-dpdgraph CI --- dev/ci/ci-basic-overlay.sh | 6 ++++++ dev/ci/ci-coq-dpdgraph.sh | 10 ++++++++++ 2 files changed, 16 insertions(+) create mode 100755 dev/ci/ci-coq-dpdgraph.sh (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index a6972c9500..8bd68f4ee6 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -112,6 +112,12 @@ : ${formal_topology_CI_BRANCH:=ci} : ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} +######################################################################## +# coq-dpdgraph +######################################################################## +: ${coq_dpdgraph_CI_BRANCH:=master} +: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} + ######################################################################## # CoLoR ######################################################################## diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh new file mode 100755 index 0000000000..44b0e4c4d5 --- /dev/null +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph + +git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} + +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) -- cgit v1.2.3 From f371ead0234693ab8f68591d160cc2ee4dd8509f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 2 Jun 2017 20:12:23 -0400 Subject: Add an overlay for coq-dpdgraph for 8.7 --- dev/ci/ci-basic-overlay.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8bd68f4ee6..73a3ba04f2 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,8 +115,11 @@ ######################################################################## # coq-dpdgraph ######################################################################## -: ${coq_dpdgraph_CI_BRANCH:=master} -: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} +# Temporary overlay +: ${coq_dpdgraph_CI_BRANCH:=trunk+clobber-test-suite} +: ${coq_dpdgraph_CI_GITURL:=https://github.com/JasonGross/coq-dpdgraph.git} +#: ${coq_dpdgraph_CI_BRANCH:=master} +#: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} ######################################################################## # CoLoR -- cgit v1.2.3 From accde4d40c89f0a40caacb9e91db61f204b05918 Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Tue, 23 Jun 2015 19:10:25 +0200 Subject: Added support for a side effect on constants in reduction functions. This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml. --- dev/doc/changes.txt | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bcda4ff50a..631b5f5aaf 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -10,6 +10,16 @@ will fail to compile now. They should switch to `Bytes.t` * ML API * +Added two functions for declaring hooks to be executed in reduction +functions when some given constants are traversed: + + declare_reduction_effect: to declare a hook to be applied when some + constant are visited during the execution of some reduction functions + (primarily cbv). + + set_reduction_effect: to declare a constant on which a given effect + hook should be called. + We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr -- cgit v1.2.3 From 29ba5cdc0ea31ea62c727f8dcf53d2c805d4bcb3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Jun 2017 13:07:00 -0400 Subject: Remove coq-dpdgraph overlay --- dev/ci/ci-basic-overlay.sh | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 73a3ba04f2..81f4c87177 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,11 +115,8 @@ ######################################################################## # coq-dpdgraph ######################################################################## -# Temporary overlay -: ${coq_dpdgraph_CI_BRANCH:=trunk+clobber-test-suite} -: ${coq_dpdgraph_CI_GITURL:=https://github.com/JasonGross/coq-dpdgraph.git} -#: ${coq_dpdgraph_CI_BRANCH:=master} -#: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} +: ${coq_dpdgraph_CI_BRANCH:=coq-trunk} +: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} ######################################################################## # CoLoR -- cgit v1.2.3 From 55ffdf526f8dbf99a88a05910e646446f6bb3421 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Jun 2017 13:08:13 -0400 Subject: Mirror dpdgraph's travis test more accurately --- dev/ci/ci-coq-dpdgraph.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index 44b0e4c4d5..e8018158bf 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) -- cgit v1.2.3 From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Mon, 29 May 2017 11:02:06 +0200 Subject: Remove (useless) aliases from the API. --- dev/top_printers.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a1b3c81b9a..6ae5125f6d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -37,7 +37,7 @@ let pp x = Pp.pp_with !Topfmt.std_ft x let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) (* name printers *) -let ppid id = pp (pr_id id) +let ppid id = pp (Id.print id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) @@ -79,12 +79,12 @@ let ppbigint n = pp (str (Bigint.to_string n));; let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset pr_id (Id.Set.elements l)) +let ppidset l = pp (prset Id.print (Id.Set.elements l)) let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" let pridmap pr l = - let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in + let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) let ppidmap pr l = pp (pridmap pr l) @@ -95,10 +95,10 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> (match copt with None -> mt () | Some c -> spc () ++ str "") ++ (if id = id0 then mt () - else spc () ++ str "")))) + else spc () ++ str "")))) -let prididmap = pridmap (fun _ -> pr_id) -let ppididmap = ppidmap (fun _ -> pr_id) +let prididmap = pridmap (fun _ -> Id.print) +let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") @@ -132,15 +132,15 @@ let safe_pr_global = function int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") - | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") + | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) @@ -538,21 +538,21 @@ let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in Qualid (Loc.tag ?loc @@ make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = repr_con cst in + let (mp,dir,id) = Constant.repr3 cst in encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "CSTR" (Some (mp,dir)) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) @@ -561,14 +561,14 @@ let raw_string_of_ref ?loc _ = function let short_string_of_ref ?loc _ = function | VarRef id -> Ident (Loc.tag ?loc id) - | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn))) + | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> - encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))] + encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None - [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that -- cgit v1.2.3 From 75f42c5c4f350f301ef1968459f4f19f7a349ad4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 11 Jun 2017 20:22:43 -0400 Subject: Point ci-hott at a newer version of HoTT --- dev/ci/ci-basic-overlay.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index a6972c9500..d75011de3f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,8 @@ ######################################################################## # HoTT ######################################################################## -# Temporal overlay -: ${HoTT_CI_BRANCH:=mz-8.7} +# Temporary overlay +: ${HoTT_CI_BRANCH:=ocaml.4.02.3} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} # : ${HoTT_CI_BRANCH:=master} # : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} -- cgit v1.2.3 From 26779fca89abd93a446a97cc888070b11960dd31 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 12 Jun 2017 11:47:37 +0200 Subject: Fix ocamldebug for the API --- dev/core.dbg | 2 ++ dev/ocamldebug-coq.run | 1 + 2 files changed, 3 insertions(+) (limited to 'dev') diff --git a/dev/core.dbg b/dev/core.dbg index 6acdd01528..71d06cdb0a 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -17,4 +17,6 @@ load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma +load_printer intf.cma +load_printer API.cma load_printer ltac_plugin.cmo diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3850c05fd9..f4799f7b2c 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -23,6 +23,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ + -I $COQTOP/API \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ -- cgit v1.2.3 From 8443867a2f944c3ecaf0b0b826368c29935a21e1 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Thu, 8 Jun 2017 18:30:18 +0200 Subject: add overlays --- dev/ci/ci-user-overlay.sh | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 195ede6d00..0edaf07efc 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -30,3 +30,13 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi +echo "DEBUG: ci-user-overlay.sh 0" +if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then + echo "DEBUG: ci-user-overlay.sh 1" + bedrock_src_CI_BRANCH=trunk__API + bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git + bedrock_facade_CI_BRANCH=trunk__API + bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git + fiat_parsers_CI_BRANCH=trunk__API + fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git +fi -- cgit v1.2.3 From 013c0232953f1f5832c30940119da05847e99ce2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 12 Jun 2017 15:43:12 +0200 Subject: Temporary overlay, waiting for upstream PR merges. --- dev/ci/ci-basic-overlay.sh | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index a6972c9500..7a9df93c45 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -85,8 +85,8 @@ ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=master} -: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} +: ${fiat_parsers_CI_BRANCH:=trunk__API} +: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git} ######################################################################## # fiat_crypto @@ -97,14 +97,14 @@ ######################################################################## # bedrock_src ######################################################################## -: ${bedrock_src_CI_BRANCH:=master} -: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} +: ${bedrock_src_CI_BRANCH:=trunk__API} +: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git} ######################################################################## # bedrock_facade ######################################################################## -: ${bedrock_facade_CI_BRANCH:=master} -: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} +: ${bedrock_facade_CI_BRANCH:=trunk__API} +: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git} ######################################################################## # formal-topology -- cgit v1.2.3 From fe972a369adf533e2f4ec89eafb63b08a26e2ec7 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 6 Jun 2017 19:45:48 +0200 Subject: [travis] adapt CoLoR compilation to depend on the bignum package --- dev/ci/ci-color.sh | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 3f0716511d..cb212e845c 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -5,6 +5,19 @@ source ${ci_dir}/ci-common.sh Color_CI_DIR=${CI_BUILD_DIR}/color +# Setup Bignums + +git_checkout master https://github.com/coq/bignums.git bignums + +( cd bignums && make -j ${NJOBS} && make install ) + +# Compiles CoLoR + svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} +sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v +sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v + ( cd ${Color_CI_DIR} && make -j ${NJOBS} ) -- cgit v1.2.3 From 08e86c0af77e83b8569fe611b9fb74e772d710a8 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 6 Jun 2017 20:47:26 +0200 Subject: [travis] overlay + extra deps for math-classes (and formal-topology) --- dev/ci/ci-formal-topology.sh | 6 ++++++ dev/ci/ci-math-classes.sh | 6 ++++++ dev/ci/ci-user-overlay.sh | 5 +++++ 3 files changed, 17 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index ecb36349fb..87171ba0bd 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -9,6 +9,12 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology +# Setup Bignums + +git_checkout master https://github.com/coq/bignums.git bignums + +( cd bignums && make -j ${NJOBS} && make install ) + # Setup Math-Classes git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index beb75773b7..10b9d7af24 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -7,6 +7,12 @@ math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes Corn_CI_DIR=${CI_BUILD_DIR}/corn +# Setup Bignums + +git_checkout master https://github.com/coq/bignums.git bignums + +( cd bignums && make -j ${NJOBS} && make install ) + # Setup Math-Classes git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 0edaf07efc..594e3c3744 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -40,3 +40,8 @@ if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_make fiat_parsers_CI_BRANCH=trunk__API fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git fi + +if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then + math_classes_CI_BRANCH=external-bignums + math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git +fi -- cgit v1.2.3 From 0fd563c07433db5aad5c5a3f196ea692bb60c04e Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 6 Jun 2017 21:22:15 +0200 Subject: [travis] extra test ci-bignums (+factorize other scripts) --- dev/ci/ci-basic-overlay.sh | 6 ++++++ dev/ci/ci-bignums.sh | 16 ++++++++++++++++ dev/ci/ci-color.sh | 4 +--- dev/ci/ci-formal-topology.sh | 4 +--- dev/ci/ci-math-classes.sh | 4 +--- 5 files changed, 25 insertions(+), 9 deletions(-) create mode 100755 dev/ci/ci-bignums.sh (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3adc319355..98d342412a 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -133,3 +133,9 @@ ######################################################################## : ${tlc_CI_BRANCH:=master} : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} + +######################################################################## +# Bignums +######################################################################## +: ${bignums_CI_BRANCH:=master} +: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh new file mode 100755 index 0000000000..ff5935d4c7 --- /dev/null +++ b/dev/ci/ci-bignums.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}"]; +then + source ${ci_dir}/ci-common.sh +fi + +bignums_CI_DIR=${CI_BUILD_DIR}/Bignums + +git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR} + +( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index cb212e845c..57f569858b 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -7,9 +7,7 @@ Color_CI_DIR=${CI_BUILD_DIR}/color # Setup Bignums -git_checkout master https://github.com/coq/bignums.git bignums - -( cd bignums && make -j ${NJOBS} && make install ) +source ${ci_dir}/ci-bignums.sh # Compiles CoLoR diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 87171ba0bd..64b78c0396 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -11,9 +11,7 @@ formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology # Setup Bignums -git_checkout master https://github.com/coq/bignums.git bignums - -( cd bignums && make -j ${NJOBS} && make install ) +source ${ci_dir}/ci-bignums.sh # Setup Math-Classes diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 10b9d7af24..46581c6381 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -9,9 +9,7 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn # Setup Bignums -git_checkout master https://github.com/coq/bignums.git bignums - -( cd bignums && make -j ${NJOBS} && make install ) +source ${ci_dir}/ci-bignums.sh # Setup Math-Classes -- cgit v1.2.3 From 268ccbb0d3d990e42cef4ae4833e0e7964aea24d Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 10 Jun 2017 17:35:10 +0200 Subject: [travis] overlay for corn --- dev/ci/ci-user-overlay.sh | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 594e3c3744..200d431bcb 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -44,4 +44,6 @@ fi if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then math_classes_CI_BRANCH=external-bignums math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git + Corn_CI_BRANCH=external-bignums + Corn_CI_GITURL=https://github.com/letouzey/corn.git fi -- cgit v1.2.3 From 7e63c300a3aa1e3befb29bab9094e8b1939824bb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 13 Jun 2017 17:22:42 +0200 Subject: Temporary overlays for bignums. --- dev/ci/ci-basic-overlay.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dev') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 98d342412a..54db58c01f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -28,11 +28,11 @@ ######################################################################## # Mathclasses + Corn ######################################################################## -: ${math_classes_CI_BRANCH:=v8.6} -: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} +: ${math_classes_CI_BRANCH:=external-bignums} +: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git} -: ${Corn_CI_BRANCH:=v8.6} -: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} +: ${Corn_CI_BRANCH:=external-bignums} +: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git} ######################################################################## # Iris -- cgit v1.2.3