# -*- 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.51.1 v
revision            0

categories          math
license             Apache-2
maintainers         {@kakuhen} openmaintainer
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  6fd7bd6c78b8988c41ee32526b1c5b6b26b0fba5 \
                    sha256  5a4734bf345d6c5ba6eacd2d33d86d9540eea7d008b4ebf8dde126e729fcbcaf \
                    size    1918894
github.tarball_from archive

# 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