From 4eddce8ce9337fd4d8f4fd97b7d41ac3cef4e3f0 Mon Sep 17 00:00:00 2001 From: Greg Hogan Date: Tue, 28 Jun 2022 15:22:47 +0000 Subject: gnu: octave: Update to 7.1.0. * gnu/packages/maths.scm (octave): Update to 7.1.0. Signed-off-by: Guillaume Le Vaillant --- gnu/packages/maths.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 5e8fd7ae2d..8268b8954e 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -2657,7 +2657,7 @@ can solve two kinds of problems: (define-public octave-cli (package (name "octave-cli") - (version "6.2.0") + (version "7.1.0") (source (origin (method url-fetch) @@ -2665,7 +2665,7 @@ can solve two kinds of problems: version ".tar.xz")) (sha256 (base32 - "06id09zspya24gshcwgp039cp35c06150mdlxysawgnbrhj16wkv")))) + "0wv26nsfi6cq80np6p4av4wfrvbaflca6szajf6c60mbpdg63m1z")))) (build-system gnu-build-system) (inputs `(("alsa-lib" ,alsa-lib) -- cgit v1.2.3 From 36a0ec9e784b74478f740474e7c3b8138372c3c3 Mon Sep 17 00:00:00 2001 From: "Jan (janneke) Nieuwenhuizen" Date: Mon, 27 Jun 2022 18:35:27 +0200 Subject: gnu: mcrl2: Update to 202206.0. * gnu/packages/patches/mcrl2-fix-1687.patch, gnu/packages/patches/mcrl2-fix-counterexample.patch: New files. * gnu/local.mk (dist_patch_DATA): Add them. * gnu/packages/maths.scm (mcrl2): Update to 202206.0 and use them. --- gnu/local.mk | 2 + gnu/packages/maths.scm | 8 +- gnu/packages/patches/mcrl2-fix-1687.patch | 337 +++++++++++++++++++++ .../patches/mcrl2-fix-counterexample.patch | 32 ++ 4 files changed, 376 insertions(+), 3 deletions(-) create mode 100644 gnu/packages/patches/mcrl2-fix-1687.patch create mode 100644 gnu/packages/patches/mcrl2-fix-counterexample.patch (limited to 'gnu/packages/maths.scm') diff --git a/gnu/local.mk b/gnu/local.mk index 353b91cfd2..3a56ad371d 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -1481,6 +1481,8 @@ dist_patch_DATA = \ %D%/packages/patches/maxima-defsystem-mkdir.patch \ %D%/packages/patches/maven-generate-component-xml.patch \ %D%/packages/patches/maven-generate-javax-inject-named.patch \ + %D%/packages/patches/mcrl2-fix-1687.patch \ + %D%/packages/patches/mcrl2-fix-counterexample.patch \ %D%/packages/patches/mcrypt-CVE-2012-4409.patch \ %D%/packages/patches/mcrypt-CVE-2012-4426.patch \ %D%/packages/patches/mcrypt-CVE-2012-4527.patch \ diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 8268b8954e..e84697c63b 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -22,7 +22,7 @@ ;;; Copyright © 2017, 2019, 2022 Arun Isaac ;;; Copyright © 2017–2021 Tobias Geerinckx-Rice ;;; Copyright © 2017 Dave Love -;;; Copyright © 2018, 2019, 2020, 2021 Jan (janneke) Nieuwenhuizen +;;; Copyright © 2018, 2019, 2020, 2021, 2022 Jan (janneke) Nieuwenhuizen ;;; Copyright © 2018 Joshua Sierles, Nextjournal ;;; Copyright © 2018 Nadya Voronova ;;; Copyright © 2018 Adam Massmann @@ -6089,15 +6089,17 @@ reduction.") (define-public mcrl2 (package (name "mcrl2") - (version "202106.0") + (version "202206.0") (source (origin (method url-fetch) (uri (string-append "https://www.mcrl2.org/download/release/mcrl2-" version ".tar.gz")) + (patches (search-patches "mcrl2-fix-1687.patch" + "mcrl2-fix-counterexample.patch")) (sha256 (base32 - "1xgx3cd57vc7gbjic24j1q2za6j3ybz6nk4afvvpbwsf33xnlf4v")))) + "0alpck09pbvwk4axqmrvcjmsabsn20yayq5b3apq284n0hcbf01q")))) (inputs (list boost glu mesa qtbase-5)) (build-system cmake-build-system) diff --git a/gnu/packages/patches/mcrl2-fix-1687.patch b/gnu/packages/patches/mcrl2-fix-1687.patch new file mode 100644 index 0000000000..449ecbf638 --- /dev/null +++ b/gnu/packages/patches/mcrl2-fix-1687.patch @@ -0,0 +1,337 @@ +Taken from upstream: + https://github.com/mCRL2org/mCRL2/commit/f38998be5198236bc5bf5a957b0e132d6d6d8bee + +Fixes bug in ltsconvert: + https://listserver.tue.nl/pipermail/mcrl2-users/2022-June/000395.html + +From f38998be5198236bc5bf5a957b0e132d6d6d8bee Mon Sep 17 00:00:00 2001 +From: Jan Friso Groote +Date: Tue, 28 Jun 2022 12:27:47 +0200 +Subject: [PATCH] Solved bug report #1687 + +Hidden actions were not properly recognized in ltsconvert. Multiactions +that were partly hidden compared with the default action label, and had +to be compared with a tau-action. This caused multiple tau-actions to be +listed in the list of actions of an lts, and this caused other tools to +go astray. + +The code to rename actions has completely be rewritten. + +This should solve #1687. + +A test have been added. +--- + libraries/lts/include/mcrl2/lts/lts.h | 95 ++++++++++++++++++++++--- + libraries/lts/test/lts_test.cpp | 61 ++++++++-------- + tools/release/ltsconvert/ltsconvert.cpp | 3 +- + 3 files changed, 116 insertions(+), 43 deletions(-) + +diff --git a/libraries/lts/include/mcrl2/lts/lts.h b/libraries/lts/include/mcrl2/lts/lts.h +index 095031e7c..8562eb900 100644 +--- a/libraries/lts/include/mcrl2/lts/lts.h ++++ b/libraries/lts/include/mcrl2/lts/lts.h +@@ -25,6 +25,7 @@ + #include + #include + #include ++#include + #include "mcrl2/lts/transition.h" + #include "mcrl2/lts/lts_type.h" + +@@ -482,40 +483,112 @@ class lts: public LTS_BASE + return; + } + ++ std::map action_rename_map; + for (labels_size_type i=0; i< num_action_labels(); ++i) + { + ACTION_LABEL_T a=action_label(i); + a.hide_actions(tau_actions); +- if (a==ACTION_LABEL_T()) ++ if (a==ACTION_LABEL_T::tau_action()) + { +- m_hidden_label_set.insert(i); ++ if (i!=const_tau_label_index) ++ { ++ m_hidden_label_set.insert(i); ++ } + } + else if (a!=action_label(i)) + { +- set_action_label(i,a); ++ /* In this the action_label i is changed by the tau_actions but not renamed to tau. ++ We check whether a maps onto another action label index. If yes, it is added to ++ the rename map, and we explicitly rename transition labels with this label afterwards. ++ If no, we rename the action label. ++ */ ++ bool found=false; ++ for (labels_size_type j=0; !found && j< num_action_labels(); ++j) ++ { ++ if (a==action_label(j)) ++ { ++ if (i!=j) ++ { ++ action_rename_map[i]=j; ++ } ++ found=true; ++ } ++ } ++ if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a. ++ { ++ set_action_label(i,a); ++ } ++ } ++ } ++ ++ if (action_rename_map.size()>0) // Check whether there are action labels that must be renamed, and ++ { ++ for(transition& t: m_transitions) ++ { ++ auto i = action_rename_map.find(t.label()); ++ if (i!=action_rename_map.end()) ++ { ++ t=transition(t.from(),i->second,t.to()); ++ } + } + } + } + +- /** \brief Apply the recorded actions that are renamed to internal actions to the lts. +- * \details After hiding actions, it checks whether action labels are +- * equal and merges actions with the same labels in the lts. ++ /** \brief Rename the hidden actions in the lts. ++ * \details Multiactions can be partially renamed. I.e. a|b becomes a if b is hidden. ++ * In such a case the new action a is mapped onto an existing action a; if such ++ * a label a does not exist, the action a|b is renamed to a. + * \param[in] tau_actions Vector with strings indicating which actions must be + * transformed to tau's */ +- void apply_hidden_actions(void) ++ void apply_hidden_actions(const std::vector& tau_actions) + { +- if (m_hidden_label_set.size()>0) // Check whether there is something to rename. ++ if (tau_actions.size()==0) ++ { ++ return; ++ } ++ ++ std::map action_rename_map; ++ for (labels_size_type i=0; i< num_action_labels(); ++i) ++ { ++ ACTION_LABEL_T a=action_label(i); ++ a.hide_actions(tau_actions); ++#ifndef NDEBUG ++ ACTION_LABEL_T b=a; ++ b.hide_actions(tau_actions); ++ assert(a==b); // hide_actions applied twice yields the same result as applying it once. ++#endif ++ bool found=false; ++ for (labels_size_type j=0; !found && j< num_action_labels(); ++j) ++ { ++ if (a==action_label(j)) ++ { ++ if (i!=j) ++ { ++ action_rename_map[i]=j; ++ } ++ found=true; ++ } ++ } ++ if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a. ++ { ++ set_action_label(i,a); ++ } ++ } ++ ++ ++ if (action_rename_map.size()>0) // Check whether there is something to rename. + { + for(transition& t: m_transitions) + { +- if (m_hidden_label_set.count(t.label())) ++ auto i = action_rename_map.find(t.label()); ++ if (i!=action_rename_map.end()) + { +- t=transition(t.from(),tau_label_index(),t.to()); ++ t=transition(t.from(),i->second,t.to()); + } + } +- m_hidden_label_set.clear(); // Empty the hidden label set. + } + } ++ + /** \brief Checks whether this LTS has state values associated with its states. + * \retval true if the LTS has state information; + * \retval false otherwise. +diff --git a/libraries/lts/test/lts_test.cpp b/libraries/lts/test/lts_test.cpp +index 5840393d9..ad69f6275 100644 +--- a/libraries/lts/test/lts_test.cpp ++++ b/libraries/lts/test/lts_test.cpp +@@ -149,7 +149,7 @@ static void reduce_lts_in_various_ways(const std::string& test_description, + BOOST_CHECK(is_deterministic(l)); + } + +-static void reduce_simple_loop() ++BOOST_AUTO_TEST_CASE(reduce_simple_loop) + { + std::string SIMPLE_AUT = + "des (0,2,2)\n" +@@ -173,7 +173,7 @@ static void reduce_simple_loop() + reduce_lts_in_various_ways("Simple loop", SIMPLE_AUT, expected); + } + +-static void reduce_simple_loop_with_tau() ++BOOST_AUTO_TEST_CASE(reduce_simple_loop_with_tau) + { + std::string SIMPLE_AUT = + "des (0,2,2)\n" +@@ -200,7 +200,7 @@ static void reduce_simple_loop_with_tau() + /* The example below was encountered by David Jansen. The problem is that + * for branching bisimulations the tau may supersede the b, not leading to the + * necessary splitting into two equivalence classes. */ +-static void tricky_example_for_branching_bisimulation() ++BOOST_AUTO_TEST_CASE(tricky_example_for_branching_bisimulation) + { + std::string TRICKY_BB = + "des (0,3,2)\n" +@@ -226,7 +226,7 @@ static void tricky_example_for_branching_bisimulation() + } + + +-static void reduce_abp() ++BOOST_AUTO_TEST_CASE(reduce_abp) + { + std::string ABP_AUT = + "des (0,92,74)\n" +@@ -342,7 +342,7 @@ static void reduce_abp() + + // Peterson's protocol has the interesting property that the number of states modulo branching bisimulation + // differs from the number of states modulo weak bisimulation, as observed by Rob van Glabbeek. +-static void reduce_peterson() ++BOOST_AUTO_TEST_CASE(reduce_peterson) + { + std::string PETERSON_AUT = + "des (0,59,35)\n" +@@ -423,7 +423,7 @@ static void reduce_peterson() + reduce_lts_in_various_ways("Peterson protocol", PETERSON_AUT, expected); + } + +-static void test_reachability() ++BOOST_AUTO_TEST_CASE(test_reachability) + { + std::string REACH = + "des (0,4,5) \n" +@@ -449,7 +449,7 @@ static void test_reachability() + + // The example below caused failures in the GW mlogn branching bisimulation + // algorithm when cleaning the code up. +-static void failing_test_groote_wijs_algorithm() ++BOOST_AUTO_TEST_CASE(failing_test_groote_wijs_algorithm) + { + std::string GWLTS = + "des(0,29,10)\n" +@@ -511,7 +511,7 @@ static void failing_test_groote_wijs_algorithm() + // It has not been implemented fully. The problem is that it is difficult to + // prescribe the order in which refinements have to be done. + +-static void counterexample_jk_1(std::size_t k) ++void counterexample_jk_1(std::size_t k) + { + // numbering scheme of states: + // states 0..k-1 are the blue squares +@@ -571,7 +571,7 @@ static void counterexample_jk_1(std::size_t k) + + // In the meantime, the bug is corrected: this is why the first part of the + // algorithm now follows a much simpler line than previously. +-static void counterexample_postprocessing() ++BOOST_AUTO_TEST_CASE(counterexample_postprocessing) + { + std::string POSTPROCESS_AUT = + "des(0,33,13)\n" +@@ -634,7 +634,7 @@ static void counterexample_postprocessing() + test_lts("postprocessing problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count); + } + +-static void regression_delete_old_bb_slice() ++BOOST_AUTO_TEST_CASE(regression_delete_old_bb_slice) + { + std::string POSTPROCESS_AUT = + "des(0,163,100)\n" +@@ -824,7 +824,7 @@ static void regression_delete_old_bb_slice() + test_lts("regression test for GJKW bug (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count); + } + +-void is_deterministic_test1() ++BOOST_AUTO_TEST_CASE(is_deterministic_test1) + { + std::string automaton = + "des(0,2,2)\n" +@@ -837,7 +837,7 @@ void is_deterministic_test1() + BOOST_CHECK(is_deterministic(l_det)); + } + +-void is_deterministic_test2() ++BOOST_AUTO_TEST_CASE(is_deterministic_test2) + { + std::string automaton = + "des(0,2,2)\n" +@@ -850,24 +850,25 @@ void is_deterministic_test2() + BOOST_CHECK(!is_deterministic(l_det)); + } + +-void test_is_deterministic() ++BOOST_AUTO_TEST_CASE(hide_actions1) + { +- is_deterministic_test1(); +- is_deterministic_test2(); +-} ++ std::string automaton = ++ "des (0,4,3)\n" ++ "(0,\"\",1)\n" ++ "(1,\"return|hello\",2)\n" ++ "(1,\"return\",2)\n" ++ "(2,\"world\",1)\n"; ++ ++ std::istringstream is(automaton); ++ lts::lts_aut_t l; ++ l.load(is); ++ std::vectorhidden_actions(1,"hello"); ++ l.apply_hidden_actions(hidden_actions); ++ reduce(l,lts::lts_eq_bisim); ++ std::size_t expected_label_count = 5; ++ std::size_t expected_state_count = 3; ++ std::size_t expected_transition_count = 3; ++ test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count); ++ + +-BOOST_AUTO_TEST_CASE(test_main) +-{ +- reduce_simple_loop(); +- reduce_simple_loop_with_tau(); +- tricky_example_for_branching_bisimulation(); +- reduce_abp(); +- reduce_peterson(); +- test_reachability(); +- test_is_deterministic(); +- failing_test_groote_wijs_algorithm(); +- counterexample_jk_1(3); +- counterexample_postprocessing(); +- regression_delete_old_bb_slice(); +- // TODO: Add groote wijs branching bisimulation and add weak bisimulation tests. For the last Peterson is a good candidate. + } +diff --git a/tools/release/ltsconvert/ltsconvert.cpp b/tools/release/ltsconvert/ltsconvert.cpp +index 231deabe2..5645d31d1 100644 +--- a/tools/release/ltsconvert/ltsconvert.cpp ++++ b/tools/release/ltsconvert/ltsconvert.cpp +@@ -123,8 +123,7 @@ class ltsconvert_tool : public input_output_tool + + LTS_TYPE l; + l.load(tool_options.infilename); +- l.record_hidden_actions(tool_options.tau_actions); +- l.apply_hidden_actions(); ++ l.apply_hidden_actions(tool_options.tau_actions); + + if (tool_options.check_reach) + { +-- +2.35.1 + diff --git a/gnu/packages/patches/mcrl2-fix-counterexample.patch b/gnu/packages/patches/mcrl2-fix-counterexample.patch new file mode 100644 index 0000000000..abf541f50c --- /dev/null +++ b/gnu/packages/patches/mcrl2-fix-counterexample.patch @@ -0,0 +1,32 @@ +Taken from upstream: + https://github.com/mCRL2org/mCRL2/commit/435421429dde9dcc5956e8a978597111a3947ec1 + +Fixes bug in ltscompare: + https://listserver.tue.nl/pipermail/mcrl2-users/2022-June/000396.html + +From 435421429dde9dcc5956e8a978597111a3947ec1 Mon Sep 17 00:00:00 2001 +From: Maurice Laveaux +Date: Wed, 29 Jun 2022 10:27:58 +0200 +Subject: [PATCH] Write counterexample's structured output trace on single + line. + +--- + libraries/lts/include/mcrl2/lts/detail/counter_example.h | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/libraries/lts/include/mcrl2/lts/detail/counter_example.h b/libraries/lts/include/mcrl2/lts/detail/counter_example.h +index c339cfde4..ca3967768 100644 +--- a/libraries/lts/include/mcrl2/lts/detail/counter_example.h ++++ b/libraries/lts/include/mcrl2/lts/detail/counter_example.h +@@ -139,7 +139,7 @@ class counter_example_constructor + if (m_structured_output) + { + std::cout << m_name << ": "; +- result.save("", mcrl2::lts::trace::tfPlain); // Write to stdout. ++ result.save("", mcrl2::lts::trace::tfLine); // Write to stdout. + } + else + { +-- +2.35.1 + -- cgit v1.2.3 From 3366be5db0d744625accc80ebc8d155bf1ddece8 Mon Sep 17 00:00:00 2001 From: Zhu Zihao Date: Mon, 20 Jun 2022 20:09:20 +0800 Subject: gnu: z3: Use G-expressions. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (z3)[arguments]: Use G-expressions. [native-inputs]: Use label-less style. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 89 +++++++++++++++++++++++++------------------------- 1 file changed, 45 insertions(+), 44 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index e84697c63b..945795a055 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -50,6 +50,7 @@ ;;; Copyright © 2021 Jean-Baptiste Volatier ;;; Copyright © 2021 Guillaume Le Vaillant ;;; Copyright © 2021 Pierre-Antoine Bouttier +;;; Copyright © 2022 Zhu Zihao ;;; ;;; This file is part of GNU Guix. ;;; @@ -5831,51 +5832,51 @@ as equations, scalars, vectors, and matrices.") "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx")))) (build-system gnu-build-system) (arguments - `(#:imported-modules ((guix build python-build-system) - ,@%gnu-build-system-modules) - #:modules (((guix build python-build-system) #:select (site-packages)) - (guix build gnu-build-system) - (guix build utils)) - #:phases - (modify-phases %standard-phases - (add-after 'unpack 'enable-bytecode-determinism - (lambda _ - (setenv "PYTHONHASHSEED" "0") - #t)) - (add-after 'unpack 'fix-compatability - ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only. - (lambda _ - (substitute* "src/util/mpz.cpp" - (("#include ") "")) - #t)) - (add-before 'configure 'bootstrap - (lambda _ - (invoke "python" "scripts/mk_make.py"))) - ;; work around gnu-build-system's setting --enable-fast-install - ;; (z3's `configure' is a wrapper around the above python file, - ;; which fails when passed --enable-fast-install) - (replace 'configure - (lambda* (#:key inputs outputs #:allow-other-keys) - (invoke "./configure" - "--python" - (string-append "--prefix=" (assoc-ref outputs "out")) - (string-append "--pypkgdir=" (site-packages inputs outputs))))) - (add-after 'configure 'change-directory - (lambda _ - (chdir "build") - #t)) - (add-before 'check 'make-test-z3 - (lambda _ - ;; Build the test suite executable. - (invoke "make" "test-z3" "-j" - (number->string (parallel-job-count))))) - (replace 'check - (lambda _ - ;; Run all the tests that don't require arguments. - (invoke "./test-z3" "/a")))))) + (list + #:imported-modules `((guix build python-build-system) + ,@%cmake-build-system-modules) + #:modules '((guix build cmake-build-system) + (guix build utils) + ((guix build python-build-system) #:select (site-packages))) + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'enable-bytecode-determinism + (lambda _ + (setenv "PYTHONHASHSEED" "0") + #t)) + (add-after 'unpack 'fix-compatability + ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only. + (lambda _ + (substitute* "src/util/mpz.cpp" + (("#include ") "")) + #t)) + (add-before 'configure 'bootstrap + (lambda _ + (invoke "python" "scripts/mk_make.py"))) + ;; work around gnu-build-system's setting --enable-fast-install + ;; (z3's `configure' is a wrapper around the above python file, + ;; which fails when passed --enable-fast-install) + (replace 'configure + (lambda* (#:key inputs outputs #:allow-other-keys) + (invoke "./configure" + "--python" + (string-append "--prefix=" (assoc-ref outputs "out")) + (string-append "--pypkgdir=" (site-packages inputs outputs))))) + (add-after 'configure 'change-directory + (lambda _ + (chdir "build") + #t)) + (add-before 'check 'make-test-z3 + (lambda _ + ;; Build the test suite executable. + (invoke "make" "test-z3" "-j" + (number->string (parallel-job-count))))) + (replace 'check + (lambda _ + ;; Run all the tests that don't require arguments. + (invoke "./test-z3" "/a")))))) (native-inputs - `(("which" ,which) - ("python" ,python-wrapper))) + (list which python-wrapper)) (synopsis "Theorem prover") (description "Z3 is a theorem prover and @dfn{satisfiability modulo theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.") -- cgit v1.2.3 From cec514218336132922ca0bf883f309fa07662b45 Mon Sep 17 00:00:00 2001 From: Zhu Zihao Date: Mon, 20 Jun 2022 20:14:37 +0800 Subject: gnu: z3: Update to 4.8.17. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (z3): Update to 4.8.17. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 945795a055..a708e2aee7 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -5820,7 +5820,7 @@ as equations, scalars, vectors, and matrices.") (define-public z3 (package (name "z3") - (version "4.8.9") + (version "4.8.17") (home-page "https://github.com/Z3Prover/z3") (source (origin (method git-fetch) @@ -5829,8 +5829,8 @@ as equations, scalars, vectors, and matrices.") (file-name (git-file-name name version)) (sha256 (base32 - "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx")))) (build-system gnu-build-system) + "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05")))) (arguments (list #:imported-modules `((guix build python-build-system) -- cgit v1.2.3 From 0e64835b2ed910a23c9312c036649f67209436e2 Mon Sep 17 00:00:00 2001 From: Zhu Zihao Date: Mon, 20 Jun 2022 20:17:54 +0800 Subject: gnu: z3: Prefer CMake to build the package. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Z3 developer recommends to use CMake to build Z3 except the OCaml bindings. Use CMake also enable us to cross compile z3. * gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system. [arguments]<#:configure-flags>: Add flags for CMake. <#:phases>: Remove stale phase 'fix-compatability'. In phase 'check', build the z3 test binary and don't test when cross compiling. Add phase 'compile-python-modules' phase to generate python bytecode cache for z3 python binding. Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3 shared library. (ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 64 ++++++++++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 33 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index a708e2aee7..6edf36d928 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -5829,8 +5829,8 @@ as equations, scalars, vectors, and matrices.") (file-name (git-file-name name version)) (sha256 (base32 - (build-system gnu-build-system) "1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05")))) + (build-system cmake-build-system) (arguments (list #:imported-modules `((guix build python-build-system) @@ -5838,43 +5838,40 @@ as equations, scalars, vectors, and matrices.") #:modules '((guix build cmake-build-system) (guix build utils) ((guix build python-build-system) #:select (site-packages))) + #:configure-flags + #~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON" + "-DZ3_LINK_TIME_OPTIMIZATION=ON" + (string-append + "-DCMAKE_INSTALL_PYTHON_PKG_DIR=" + #$output "/lib/python" + #$(version-major+minor (package-version python-wrapper)) + "/site-packages")) #:phases #~(modify-phases %standard-phases - (add-after 'unpack 'enable-bytecode-determinism + (replace 'check + (lambda* (#:key parallel-build? tests? #:allow-other-keys) + (when tests? + (invoke "make" "test-z3" + (format #f "-j~a" + (if parallel-build? + (parallel-job-count) + 1))) + (invoke "./test-z3" "/a")))) + (add-after 'install 'compile-python-modules (lambda _ (setenv "PYTHONHASHSEED" "0") - #t)) - (add-after 'unpack 'fix-compatability - ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only. - (lambda _ - (substitute* "src/util/mpz.cpp" - (("#include ") "")) - #t)) - (add-before 'configure 'bootstrap - (lambda _ - (invoke "python" "scripts/mk_make.py"))) - ;; work around gnu-build-system's setting --enable-fast-install - ;; (z3's `configure' is a wrapper around the above python file, - ;; which fails when passed --enable-fast-install) - (replace 'configure + + (invoke "python" "-m" "compileall" + "--invalidation-mode=unchecked-hash" + #$output))) + ;; This step is missing in the CMake build system, do it here. + (add-after 'compile-python-modules 'fix-z3-library-path (lambda* (#:key inputs outputs #:allow-other-keys) - (invoke "./configure" - "--python" - (string-append "--prefix=" (assoc-ref outputs "out")) - (string-append "--pypkgdir=" (site-packages inputs outputs))))) - (add-after 'configure 'change-directory - (lambda _ - (chdir "build") - #t)) - (add-before 'check 'make-test-z3 - (lambda _ - ;; Build the test suite executable. - (invoke "make" "test-z3" "-j" - (number->string (parallel-job-count))))) - (replace 'check - (lambda _ - ;; Run all the tests that don't require arguments. - (invoke "./test-z3" "/a")))))) + (let* ((dest (string-append (site-packages inputs outputs) + "/z3/lib/libz3.so")) + (z3-lib (string-append #$output "/lib/libz3.so"))) + (mkdir-p (dirname dest)) + (symlink z3-lib dest))))))) (native-inputs (list which python-wrapper)) (synopsis "Theorem prover") @@ -5886,6 +5883,7 @@ theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.") (package (inherit z3) (name "ocaml-z3") + (build-system gnu-build-system) (arguments `(#:imported-modules ((guix build python-build-system) ,@%gnu-build-system-modules) -- cgit v1.2.3 From e8e7b4cdae251abebf4ae139d02e8369cc90fd01 Mon Sep 17 00:00:00 2001 From: Sharlatan Hellseher Date: Sun, 26 Jun 2022 22:28:33 +0100 Subject: gnu: Add giza MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (giza): New variable. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 6edf36d928..36431a4be8 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -51,6 +51,7 @@ ;;; Copyright © 2021 Guillaume Le Vaillant ;;; Copyright © 2021 Pierre-Antoine Bouttier ;;; Copyright © 2022 Zhu Zihao +;;; Copyright © 2022 Sharlatan Hellseher ;;; ;;; This file is part of GNU Guix. ;;; @@ -1092,6 +1093,31 @@ a pipe or file, make a variety of transformations, and render the result in the terminal or with an external viewer.") (license license:gpl1+))) ;any version +(define-public giza + (package + (name "giza") + (version "1.3.2") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/danieljprice/giza") + (commit (string-append "v" version)))) + (sha256 + (base32 "1clklh3nzgwrwg80h3k5x65gdymbvcc84c44nql7m4bv9b8rqfsq")) + (file-name (git-file-name name version)))) + (build-system gnu-build-system) + (native-inputs + (list perl pkg-config)) + (inputs + (list cairo freetype gfortran)) + (home-page "https://danieljprice.github.io/giza/") + (synopsis "Scientific plotting library for C/Fortran") + (description + "Giza is a lightweight scientific plotting library built on top of +@code{cairo} that provides uniform output to multiple devices.") + (license license:gpl2+))) + (define-public gnuplot (package (name "gnuplot") -- cgit v1.2.3 From c3a2d354e3091a94819fb2dccd515b5eaa3048ac Mon Sep 17 00:00:00 2001 From: Nicolas Goaziou Date: Mon, 4 Jul 2022 15:19:11 +0200 Subject: gnu: nauty: Update to 2.7r4. * gnu/packages/maths.scm (nauty): Update to 2.7r4. --- gnu/packages/maths.scm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 36431a4be8..a8a42579c7 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7030,7 +7030,7 @@ management via the GIMPS project's Primenet server.") (define-public nauty (package (name "nauty") - (version "2.7r3") + (version "2.7r4") (source (origin (method url-fetch) @@ -7038,7 +7038,7 @@ management via the GIMPS project's Primenet server.") "https://pallini.di.uniroma1.it/" "nauty" (string-join (string-split version #\.) "") ".tar.gz")) (sha256 - (base32 "1hl81gpf3xjf809w04jczvilq1ixy9ch1qrax8a7lgx52svna1jg")))) + (base32 "19j8i10cgnqavphj0p7kq939azxckj9ayjpjr6sg76g2dxdch45q")))) (build-system gnu-build-system) (outputs '("out" "lib")) (arguments -- cgit v1.2.3 From c0f62879744e737c5ab1dfebc69a769a2152b652 Mon Sep 17 00:00:00 2001 From: Nicolas Goaziou Date: Mon, 4 Jul 2022 15:22:03 +0200 Subject: gnu: nauty: Update package style. * gnu/packages/maths.scm (nauty)[arguments]: Use G-expressions. Remove trailing #T. --- gnu/packages/maths.scm | 76 ++++++++++++++++++++++++-------------------------- 1 file changed, 37 insertions(+), 39 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index a8a42579c7..9869fa9283 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -7042,46 +7042,44 @@ management via the GIMPS project's Primenet server.") (build-system gnu-build-system) (outputs '("out" "lib")) (arguments - `(#:test-target "checks" - #:configure-flags '("--enable-generic") ;prevent -march-native - #:phases - (modify-phases %standard-phases - ;; Default make target does not build all available - ;; executables. Create them now. - (add-after 'build 'build-extra-programs - (lambda _ - (for-each (lambda (target) (invoke "make" target)) - '("blisstog" "bliss2dre" "checks6" "sumlines")) - #t)) - ;; Upstream does not provide any install target. - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (let* ((out (assoc-ref outputs "out")) - (lib-output (assoc-ref outputs "lib")) - (bin (string-append out "/bin")) - (doc (string-append out "/share/doc/nauty/")) - (include (string-append lib-output "/include/nauty")) - (lib (string-append lib-output "/lib/nauty"))) - (for-each (lambda (f) (install-file f bin)) - '("addedgeg" "amtog" "assembleg" "biplabg" "blisstog" - "bliss2dre" "catg" "checks6" "complg" "converseg" - "copyg" "countg" "cubhamg" "deledgeg" "delptg" - "directg" "dreadnaut" "dretodot" "dretog" "genbg" - "genbgL" "geng" "genquarticg" "genrang" "genspecialg" - "gentourng" "gentreeg" "hamheuristic" "labelg" - "linegraphg" "listg" "multig" "newedgeg" "pickg" - "planarg" "ranlabg" "shortg" "showg" "subdivideg" - "sumlines" "twohamg" "underlyingg" "vcolg" - "watercluster2" "NRswitchg")) - (for-each (lambda (f) (install-file f include)) - (find-files "." "\\.h$")) - (for-each (lambda (f) (install-file f lib)) - (find-files "." "\\.a$")) - (for-each (lambda (f) (install-file f doc)) - (append '("formats.txt" "README" "schreier.txt") - (find-files "." "\\.pdf$"))))))))) + (list + #:test-target "checks" + #:configure-flags #~(list "--enable-generic") ;prevent -march-native + #:phases + #~(modify-phases %standard-phases + ;; Default make target does not build all available + ;; executables. Create them now. + (add-after 'build 'build-extra-programs + (lambda _ + (for-each (lambda (target) (invoke "make" target)) + '("blisstog" "bliss2dre" "checks6" "sumlines")))) + ;; Upstream does not provide any install target. + (replace 'install + (lambda _ + (let* ((bin (string-append #$output "/bin")) + (doc (string-append #$output "/share/doc/nauty/")) + (include (string-append #$output:lib "/include/nauty")) + (lib (string-append #$output:lib "/lib/nauty"))) + (for-each (lambda (f) (install-file f bin)) + '("addedgeg" "amtog" "assembleg" "biplabg" "blisstog" + "bliss2dre" "catg" "checks6" "complg" "converseg" + "copyg" "countg" "cubhamg" "deledgeg" "delptg" + "directg" "dreadnaut" "dretodot" "dretog" "genbg" + "genbgL" "geng" "genquarticg" "genrang" "genspecialg" + "gentourng" "gentreeg" "hamheuristic" "labelg" + "linegraphg" "listg" "multig" "newedgeg" "pickg" + "planarg" "ranlabg" "shortg" "showg" "subdivideg" + "sumlines" "twohamg" "underlyingg" "vcolg" + "watercluster2" "NRswitchg")) + (for-each (lambda (f) (install-file f include)) + (find-files "." "\\.h$")) + (for-each (lambda (f) (install-file f lib)) + (find-files "." "\\.a$")) + (for-each (lambda (f) (install-file f doc)) + (append '("formats.txt" "README" "schreier.txt") + (find-files "." "\\.pdf$"))))))))) (inputs - (list gmp)) ;for sumlines + (list gmp)) ;for sumlines (home-page "https://pallini.di.uniroma1.it/") (synopsis "Library for graph automorphisms") (description "@code{nauty} (No AUTomorphisms, Yes?) is a set of -- cgit v1.2.3 From 734f50c31dddc75dca13e2c81abf0ad5b5433e29 Mon Sep 17 00:00:00 2001 From: Maxim Cournoyer Date: Wed, 13 Jul 2022 01:07:38 -0400 Subject: gnu: elpa: Update source URL. Fixes . * gnu/packages/maths.scm (elpa): Update source URL. Reported-by: Danny Milosavljevic --- gnu/packages/maths.scm | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 9869fa9283..83a04f7301 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -5971,7 +5971,8 @@ theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.") (version "2018.11.001") (source (origin (method url-fetch) - (uri (string-append "http://elpa.mpcdf.mpg.de/html/Releases/" + (uri (string-append "https://elpa.mpcdf.mpg.de/software/" + "tarball-archive/Releases/" version "/elpa-" version ".tar.gz")) (sha256 (base32 -- cgit v1.2.3 From d10af3fc9760bb5de99f18a6e5c3709698855edc Mon Sep 17 00:00:00 2001 From: "Paul A. Patience" Date: Thu, 14 Jul 2022 19:47:55 +0000 Subject: gnu: gmsh: Remove input labels. * gnu/packages/maths.scm (gmsh)[inputs]: Remove labels. Signed-off-by: Christopher Baines --- gnu/packages/maths.scm | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 83a04f7301..18fcf4d99b 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -2984,9 +2984,9 @@ This is the certified version of the Open Cascade Technology (OCCT) library.") metis opencascade-occt)) (inputs - `(("fontconfig" ,fontconfig) - ("libxft" ,libxft) - ("python" ,python))) + (list fontconfig + libxft + python)) (arguments `(#:configure-flags `("-DENABLE_SYSTEM_CONTRIB:BOOL=ON" "-DENABLE_BUILD_SHARED:BOOL=ON" -- cgit v1.2.3 From ab636bde18079fcff205271bfba760d86f8d839b Mon Sep 17 00:00:00 2001 From: "Paul A. Patience" Date: Thu, 14 Jul 2022 19:50:29 +0000 Subject: gnu: gmsh: Remove trailing booleans. * gnu/packages/maths.scm (gmsh)[snippet, arguments]: Remove trailing booleans. Signed-off-by: Christopher Baines --- gnu/packages/maths.scm | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 18fcf4d99b..b3fe262204 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -2967,9 +2967,7 @@ This is the certified version of the Open Cascade Technology (OCCT) library.") (base32 "0asd9p64ng5l2zk5glc33x3ynnvdpndlflg3q9mr0jxr7y9x0lrm")) (modules '((guix build utils))) (snippet - '(begin - (delete-file-recursively "contrib/metis") - #t)))) + '(delete-file-recursively "contrib/metis")))) (build-system cmake-build-system) (propagated-inputs (list fltk @@ -3014,8 +3012,7 @@ This is the certified version of the Open Cascade Technology (OCCT) library.") "/lib/libgmsh.so"))) (substitute* "api/gmsh.py" (("find_library\\(\"gmsh\"\\)") - (simple-format #f "\"~a\"" libgmsh)))) - #t))))) + (simple-format #f "\"~a\"" libgmsh))))))))) (home-page "http://gmsh.info/") (synopsis "3D finite element grid generator") (description "Gmsh is a 3D finite element grid generator with a built-in -- cgit v1.2.3 From fa21cd31cb4c7002dfd2d928e4f26649b27404a1 Mon Sep 17 00:00:00 2001 From: "Paul A. Patience" Date: Thu, 14 Jul 2022 19:50:37 +0000 Subject: gnu: gmsh: Update to 4.10.5. * gnu/packages/maths.scm (gmsh): Update to 4.10.5. [source]: Reindent. Signed-off-by: Christopher Baines --- gnu/packages/maths.scm | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'gnu/packages/maths.scm') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index b3fe262204..6a84f47468 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -2953,21 +2953,21 @@ This is the certified version of the Open Cascade Technology (OCCT) library.") (define-public gmsh (package (name "gmsh") - (version "4.9.5") + (version "4.10.5") (source (origin - (method git-fetch) - (uri (git-reference - (url "https://gitlab.onelab.info/gmsh/gmsh.git") - (commit - (string-append "gmsh_" - (string-replace-substring version "." "_"))))) - (file-name (git-file-name name version)) - (sha256 - (base32 "0asd9p64ng5l2zk5glc33x3ynnvdpndlflg3q9mr0jxr7y9x0lrm")) - (modules '((guix build utils))) - (snippet - '(delete-file-recursively "contrib/metis")))) + (method git-fetch) + (uri (git-reference + (url "https://gitlab.onelab.info/gmsh/gmsh.git") + (commit + (string-append "gmsh_" + (string-replace-substring version "." "_"))))) + (file-name (git-file-name name version)) + (sha256 + (base32 "08p39yjgf3lbnjg90skpmsq9n1a9pmwppdmy5s94dc6sq2nfr7xl")) + (modules '((guix build utils))) + (snippet + '(delete-file-recursively "contrib/metis")))) (build-system cmake-build-system) (propagated-inputs (list fltk -- cgit v1.2.3