abella: update to 2.0.8.3; new deps added: ocaml-base64, -crunch, -ptime

barracuda156 · Jul 8, 2024 · d796244 · d796244
1 parent b85d7e1
commit d796244
Show file tree

Hide file tree

Showing 5 changed files with 109 additions and 42 deletions.
diff --git a/math/abella/Portfile b/math/abella/Portfile
@@ -1,10 +1,10 @@
 # -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
 
 PortSystem          1.0
-PortGroup           ocaml 1.1
+PortGroup           github 1.0
+
+github.setup        abella-prover abella 2.0.8.3 v
 
-name                abella
-version             2.0.7
 revision            0
 categories          math ocaml
 maintainers         {@barracuda156 gmail.com:vital.had} openmaintainer
@@ -14,37 +14,57 @@ long_description    Abella is an interactive theorem prover based on lambda-tree
                     This means that Abella is well-suited for reasoning about the meta-theory \
                     of programming languages and other logical systems which manipulate objects with binding.
 homepage            https://abella-prover.org
-master_sites        https://abella-prover.org/distributions
 
-checksums           rmd160  f6ea41a4def908c9ec9c44d8ad207d756fc5f8f2 \
-                    sha256  fde3a279b3051e0aeeaedad21cf96064edf19a6c413949b2033b305d92dddd87 \
-                    size    215056
+checksums           rmd160  f80f8241eb543d515ed45c43a6cd45c40336595c \
+                    sha256  b2a67a8c8a275ac46c2f4578b29068386ffa180c5b37ffa539d217193f37c185 \
+                    size    258223
+github.tarball_from archive
 
 depends_build-append \
-                    port:gmake \
-                    port:ocaml-findlib \
-                    port:ocaml-ocamlbuild
+                    port:ocaml \
+                    port:ocaml-crunch \
+                    port:ocaml-dune
 
-patchfiles          patch-bytecode.diff
+depends_lib-append  port:ocaml-base64 \
+                    port:ocaml-cmdliner \
+                    port:ocaml-menhir \
+                    port:ocaml-re \
+                    port:ocaml-yojson
 
-post-patch {
-    reinplace "s|4-29-40-41-42-44-45-48-58-59-60|4-29-40-41-42-44-45-48-58-59-60-70|" \
-                    ${worksrcpath}/myocamlbuild.ml
-}
+depends_test-append port:ocaml-ounit2
 
-use_configure       no
+build.env-append    DUNE_CONFIG__COPY_FILE=portable
+
+# https://github.com/abella-prover/abella/issues/151
+if {${configure.build_arch} in [list ppc ppc64]} {
+    build.env-append \
+                    BYTECODE=true
+    # Manual destroot does not need this, but keep it.
+    # destroot.env-append \
+                    BYTECODE=true
 
-if {${build_arch} in [list ppc ppc64]} {
-    build.target    byte
-    test.target     test_byte
+    set exe_suf     .bc
 } else {
-    build.target    all
-    test.target     test
+    set exe_suf     .exe
 }
 
+use_configure       no
+use_parallel_build  no
+
+build.target        all-release abella.install
+
 destroot {
-    xinstall -m 755 -d ${destroot}${prefix}/bin
-    file copy ${worksrcpath}/${name} ${destroot}${prefix}/bin/${name}
+    foreach bin { abella abella_dep abella_doc } {
+        copy ${worksrcpath}/_build/default/src/${bin}${exe_suf} ${destroot}${prefix}/bin/
+    }
+    xinstall -d ${destroot}${prefix}/share/${name}
+    xinstall -d ${destroot}${prefix}/share/man
+    foreach f { abella.1 abella_dep.1 abella_doc.1 } {
+        copy ${worksrcpath}/_build/default/src/${f} ${destroot}${prefix}/share/man/
+    }
+    copy ${worksrcpath}/emacs ${destroot}${prefix}/share/${name}/
+    copy ${worksrcpath}/examples ${destroot}${prefix}/share/${name}/
+    xinstall -m 0644 -W ${worksrcpath} CHANGES.md LICENSE README.md ${destroot}${prefix}/share/${name}/
 }
 
 test.run            yes

diff --git a/math/abella/files/patch-bytecode.diff b/math/abella/files/patch-bytecode.diff
diff --git a/ocaml/ocaml-base64/Portfile b/ocaml/ocaml-base64/Portfile
@@ -0,0 +1,20 @@
+# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
+
+PortSystem          1.0
+PortGroup           github 1.0
+PortGroup           ocaml 1.1
+
+github.setup        mirage ocaml-base64 3.5.1 v
+revision            0
+categories          ocaml devel
+maintainers         {@barracuda156 gmail.com:vital.had} openmaintainer
+license             ISC
+description         Base64 encoding for OCaml
+long_description    {*}${description}
+
+checksums           rmd160  7671d69089499e6cafc531fc1d62d3069111e11c \
+                    sha256  f3e8b9be43567689064b419fa5eefd9c758f00b864e9f731a0dbc1b9fecfc768 \
+                    size    18986
+github.tarball_from archive
+
+ocaml.build_type    dune
diff --git a/ocaml/ocaml-crunch/Portfile b/ocaml/ocaml-crunch/Portfile
@@ -0,0 +1,23 @@
+# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
+
+PortSystem          1.0
+PortGroup           github 1.0
+PortGroup           ocaml 1.1
+
+github.setup        mirage ocaml-crunch 3.3.1 v
+revision            0
+categories          ocaml devel
+maintainers         {@barracuda156 gmail.com:vital.had} openmaintainer
+license             ISC
+description         Convert a filesystem into a static OCaml module
+long_description    {*}${description}
+
+checksums           rmd160  639162a5fc8cbe8fe6826e6a3fcc110583080bc4 \
+                    sha256  998780470dad97099caa485f5783eed6fd8f643cec00840042938646b91eb04d \
+                    size    60602
+github.tarball_from archive
+
+depends_lib-append  port:ocaml-cmdliner \
+                    port:ocaml-ptime
+
+ocaml.build_type    dune
diff --git a/ocaml/ocaml-ptime/Portfile b/ocaml/ocaml-ptime/Portfile
@@ -0,0 +1,23 @@
+# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
+
+PortSystem          1.0
+PortGroup           github 1.0
+PortGroup           ocaml 1.1
+
+name                ocaml-ptime
+github.setup        dbuenzli ptime 1.1.0 v
+categories          ocaml devel
+maintainers         {@barracuda156 gmail.com:vital.had} openmaintainer
+license             ISC
+description         POSIX time for OCaml
+long_description    {*}${description}
+homepage            https://erratique.ch/software/ptime
+
+checksums           rmd160  c40495d3ff1b5868e0c7ca29d46f55ef73766863 \
+                    sha256  09bcfbb0fb1c4bb4b8c23f94a26e7e813d1059452f9f44b5ab7154ef8e40f32d \
+                    size    36927
+github.tarball_from archive
+
+depends_lib-append  port:ocaml-cmdliner
+
+ocaml.build_type    topkg