# -*- 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           cmake 1.1
PortGroup           github 1.0
PortGroup           compiler_blacklist_versions 1.0

github.setup        leanprover-community lean 3.50.3 v
revision            0

categories          math
license             Apache-2
maintainers         {@kakuhen} openmaintainer
platforms           darwin
supported_archs     x86_64 arm64
description         The Lean theorem prover.
long_description    A fork of Lean 3 maintained and updated by the Lean \
    community. Lean is a functional programming language that makes it easy to \
    write correct and maintainable code. You can also use Lean as an \
    interactive theorem prover.

depends_lib-append  port:gmp

checksums           rmd160  97407c039a0099caf6b38342b32d59a2980a115c \
                    sha256  0e66ce9b77857640c56c6b45e0d84683ea1edc1713d2ab531394c7a6b348d5e8 \
                    size    1918719

# use older MACH defines on systems before 10.8
patchfiles          patch-lean-util-memory-older-MACH-defines.diff

cmake.build_type    Release
cmake.generator     Ninja

set worksrcdir      ${worksrcdir}/src

compiler.cxx_standard           2011
compiler.thread_local_storage   yes


#src/frontends/lean/widget.cpp:436:24: error: use of overloaded operator '+=' is ambiguous (with operand types 'std::string' (aka 'basic_string<char, char_traits<char>, allocator<char> >') and 'lean::json' (aka 'basic_json<>'))
#                    cn += value;
#                    ~~ ^  ~~~~~

compiler.blacklist-append       {clang < 1001}

test.run            yes
test.cmd            ninja
test.target         test