[PR PATCH] New package: lean-community-3.32.1

[PR PATCH] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1596 bytes --]

There is a new pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 1113 bytes --]

From c1000540e5be5c7633a57ac9df15b795c66ce3bc Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..607e2c8e9e1e
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+depends="gmp"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 2002 bytes --]

From c1000540e5be5c7633a57ac9df15b795c66ce3bc Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH 1/2] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..607e2c8e9e1e
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+depends="gmp"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 021bb2f53ce1505f49118924f13fc1acacfe7327 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Tue, 17 Aug 2021 23:48:23 +0200
Subject: [PATCH 2/2] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index 607e2c8e9e1e..d5fe118b2ab0 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -11,7 +11,7 @@ makedepends="gmp-devel"
 depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
-license="Apache"
+license="Apache-2.0"
 homepage="https://github.com/leanprover-community/lean"
 distfiles="${homepage}/archive/v${version}.tar.gz"
 checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 2618 bytes --]

From c1000540e5be5c7633a57ac9df15b795c66ce3bc Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH 1/3] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..607e2c8e9e1e
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+depends="gmp"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 021bb2f53ce1505f49118924f13fc1acacfe7327 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Tue, 17 Aug 2021 23:48:23 +0200
Subject: [PATCH 2/3] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index 607e2c8e9e1e..d5fe118b2ab0 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -11,7 +11,7 @@ makedepends="gmp-devel"
 depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
-license="Apache"
+license="Apache-2.0"
 homepage="https://github.com/leanprover-community/lean"
 distfiles="${homepage}/archive/v${version}.tar.gz"
 checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 4d4e5ea21a9b433010256419709382882e767fec Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Wed, 18 Aug 2021 05:24:06 +0200
Subject: [PATCH 3/3] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index d5fe118b2ab0..ceef8d25f6e7 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -1,4 +1,4 @@
-# Template file for 'lean'
+# Template file for 'lean-community'
 pkgname=lean-community
 version=3.32.1
 revision=1

Re: [PR REVIEW] New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 236 bytes --]

New review comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#discussion_r692514240

Comment:
The runtime dependency on `gmp`  is not needed, it should be automatic based on sonames.

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 3371 bytes --]

From c1000540e5be5c7633a57ac9df15b795c66ce3bc Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH 1/4] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..607e2c8e9e1e
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+depends="gmp"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 021bb2f53ce1505f49118924f13fc1acacfe7327 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Tue, 17 Aug 2021 23:48:23 +0200
Subject: [PATCH 2/4] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index 607e2c8e9e1e..d5fe118b2ab0 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -11,7 +11,7 @@ makedepends="gmp-devel"
 depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
-license="Apache"
+license="Apache-2.0"
 homepage="https://github.com/leanprover-community/lean"
 distfiles="${homepage}/archive/v${version}.tar.gz"
 checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 4d4e5ea21a9b433010256419709382882e767fec Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Wed, 18 Aug 2021 05:24:06 +0200
Subject: [PATCH 3/4] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index d5fe118b2ab0..ceef8d25f6e7 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -1,4 +1,4 @@
-# Template file for 'lean'
+# Template file for 'lean-community'
 pkgname=lean-community
 version=3.32.1
 revision=1

From db5386b1980049872401a469e553585485159e6b Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Fri, 20 Aug 2021 00:01:51 +0200
Subject: [PATCH 4/4] New package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 1 -
 1 file changed, 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index ceef8d25f6e7..61fa41a6e5e5 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -8,7 +8,6 @@ build_style=cmake
 make_cmd=ninja
 hostmakedepends="cmake ninja gmp"
 makedepends="gmp-devel"
-depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
 license="Apache-2.0"

Re: [PR REVIEW] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 168 bytes --]

New review comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#discussion_r692516489

Comment:
Thanks, I removed it.

Re: New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 858 bytes --]

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-902295295

Comment:
It seems the build tries to run `lean` itself (to compile some lean files?) meaning that it's not obvious how to cross-build. Unless there's another way, you should add `nocross=yes` to template (right after `checksum`).

I compiled the template in x86_64, x86_64-musl, and i686.

All 1414 tests pass, installs and works in x86_64. Same for -musl (tested in a chroot).

I had 1 test failure in i686:
```
[...]
99% tests passed, 1 tests failed out of 1414

Total Test time (real) = 391.49 sec

The following tests FAILED:
	1340 - leanittest_complete_trailing_period.lean (Failed)
Errors while running CTest
FAILED: CMakeFiles/test.util
[...]
```

@ericonr can you approve the workflow for this PR?

Re: New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 1097 bytes --]

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-902297110

Comment:
Here's the complete error for test #1340 on i686, in case you can figure out what's wrong.
```
1340/1414 Test #1340: leanittest_complete_trailing_period.lean ....................***Failed    0.03 sec
--- complete_trailing_period.lean.expected.out	2021-08-12 10:56:43.000000000 +0000
+++ complete_trailing_period.lean.produced.out	2021-08-19 22:20:09.954646641 +0000
@@ -1,2 +1,2 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"completions":[{"source":,"text":"foo.rec","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"source":{"column":10,"line":3},"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6}
+{"completions":[],"prefix":"foo.","response":"ok","seq_num":6}
ERROR: file complete_trailing_period.lean.produced.out does not match complete_trailing_period.lean.expected.out
```

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 4092 bytes --]

From c1000540e5be5c7633a57ac9df15b795c66ce3bc Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH 1/5] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..607e2c8e9e1e
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+depends="gmp"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 021bb2f53ce1505f49118924f13fc1acacfe7327 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Tue, 17 Aug 2021 23:48:23 +0200
Subject: [PATCH 2/5] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index 607e2c8e9e1e..d5fe118b2ab0 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -11,7 +11,7 @@ makedepends="gmp-devel"
 depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
-license="Apache"
+license="Apache-2.0"
 homepage="https://github.com/leanprover-community/lean"
 distfiles="${homepage}/archive/v${version}.tar.gz"
 checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2

From 4d4e5ea21a9b433010256419709382882e767fec Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Wed, 18 Aug 2021 05:24:06 +0200
Subject: [PATCH 3/5] Update template

---
 srcpkgs/lean-community/template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index d5fe118b2ab0..ceef8d25f6e7 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -1,4 +1,4 @@
-# Template file for 'lean'
+# Template file for 'lean-community'
 pkgname=lean-community
 version=3.32.1
 revision=1

From db5386b1980049872401a469e553585485159e6b Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Fri, 20 Aug 2021 00:01:51 +0200
Subject: [PATCH 4/5] New package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 1 -
 1 file changed, 1 deletion(-)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index ceef8d25f6e7..61fa41a6e5e5 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -8,7 +8,6 @@ build_style=cmake
 make_cmd=ninja
 hostmakedepends="cmake ninja gmp"
 makedepends="gmp-devel"
-depends="gmp"
 short_desc="Lean Theorem Prover, maintained by the Lean community"
 maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
 license="Apache-2.0"

From cec31b4a257c22ba015227af533addd2375246b9 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloi.torrentsj@gmail.com>
Date: Fri, 20 Aug 2021 08:43:48 +0200
Subject: [PATCH 5/5] New package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 1 +
 1 file changed, 1 insertion(+)

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
index 61fa41a6e5e5..2ce80e6bc1cd 100644
--- a/srcpkgs/lean-community/template
+++ b/srcpkgs/lean-community/template
@@ -14,3 +14,4 @@ license="Apache-2.0"
 homepage="https://github.com/leanprover-community/lean"
 distfiles="${homepage}/archive/v${version}.tar.gz"
 checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2
+nocross=yes

Re: New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 479 bytes --]

New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-902472145

Comment:
> It seems the build tries to run `lean` itself (to compile some lean files?) meaning that it's not obvious how to cross-build. Unless there's another way, you should add `nocross=yes` to template (right after `checksum`).
> 

Done. When I know more about compiling and void I'll try to figure out if it's possible to cross-compile it.

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 1125 bytes --]

From 5ecfb3d0b7bc28197efc772bcbf6df4ec27bb5b1 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..2ce80e6bc1cd
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean-community'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache-2.0"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2
+nocross=yes

Re: New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 675 bytes --]

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-902655042

Comment:
Could you try to figure out what's the issue with the failing test in i686?

Here's how I easily test i686. In my void-packages I have a script named `xbps-src-i686` as follows:
```sh
#! /bin/sh

if [ "$1" = "binary-bootstrap" ] ; then
    set -- binary-bootstrap i686
fi

./xbps-src -m masterdir.i686 "$@"
```
Then you just use `./xbps-src-i686` instead of `./xbps-src`  (remember to run `./xbps-src-i686 binary-bootstrap` once to begin).

You can do the same for musl by replacing `i686` with `x86_64-musl`.

Re: New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 459 bytes --]

New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-904570417

Comment:
I get a lot of warnings like
```
=> WARNING: lean-community-3.32.1_1: removed empty dir: /usr/include/lean_ext/tests/util/numerics
=> WARNING: lean-community-3.32.1_1: removed empty dir: /usr/include/lean_ext/tests/util
=> WARNING: lean-community-3.32.1_1: removed empty dir: /usr/include/lean_ext/tests/shell
```

Re: New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 286 bytes --]

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-904613035

Comment:
Those warnings seem harmless. The only issue I see here is to figure out what's going on with the test on i686, and either fix it or disable it.

Re: [PR PATCH] [Updated] New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1601 bytes --]

There is an updated pull request by Eloitor against master on the void-packages repository

https://github.com/Eloitor/void-packages lean-community
https://github.com/void-linux/void-packages/pull/32559

New package: lean-community-3.32.1
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl



A patch file from https://github.com/void-linux/void-packages/pull/32559.patch is attached

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: github-pr-lean-community-32559.patch --]
[-- Type: text/x-diff, Size: 1125 bytes --]

From 5ecfb3d0b7bc28197efc772bcbf6df4ec27bb5b1 Mon Sep 17 00:00:00 2001
From: Eloi Torrents <eloitorrentsj@gmail.com>
Date: Tue, 17 Aug 2021 19:50:00 +0200
Subject: [PATCH] new package: lean-community 3.32.1

---
 srcpkgs/lean-community/template | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 srcpkgs/lean-community/template

diff --git a/srcpkgs/lean-community/template b/srcpkgs/lean-community/template
new file mode 100644
index 000000000000..2ce80e6bc1cd
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,17 @@
+# Template file for 'lean-community'
+pkgname=lean-community
+version=3.32.1
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+make_cmd=ninja
+hostmakedepends="cmake ninja gmp"
+makedepends="gmp-devel"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Eloi Torrents <eloitorrentsj@gmail.com>"
+license="Apache-2.0"
+homepage="https://github.com/leanprover-community/lean"
+distfiles="${homepage}/archive/v${version}.tar.gz"
+checksum=67acd4969baea6f4ed24dd7148ff10924c5de881fee133926414aeabf4cb53e2
+nocross=yes

Re: New package: lean-community-3.32.1

[tornaria]

[-- Attachment #1: Type: text/plain, Size: 245 bytes --]

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/32559#issuecomment-1046110504

Comment:
The test failure on i686 still happens on current version of lean (3.39.2), I've reported it upstream.

Re: [PR PATCH] [Closed]: New package: lean-community-3.32.1

[Eloitor]

[-- Attachment #1: Type: text/plain, Size: 1438 bytes --]

There's a closed pull request on the void-packages repository

New package: lean-community-3.32.1
https://github.com/void-linux/void-packages/pull/32559

Description:
<!-- Mark items with [x] where applicable -->

#### General
- [x] This is a new package and it conforms to the [quality requirements](https://github.com/void-linux/void-packages/blob/master/Manual.md#quality-requirements)

#### Have the results of the proposed changes been tested?
- [x] I use the packages affected by the proposed changes on a regular basis and confirm this PR works for me
- [ ] I generally don't use the affected packages but briefly tested this PR

<!--
If GitHub CI cannot be used to validate the build result (for example, if the
build is likely to take several hours), make sure to
[skip CI](https://github.com/void-linux/void-packages/blob/master/CONTRIBUTING.md#continuous-integration).
When skipping CI, uncomment and fill out the following section.
Note: for builds that are likely to complete in less than 2 hours, it is not
acceptable to skip CI.
-->
 
#### Does it build and run successfully? 
(Please choose at least one native build and, if supported, at least one cross build. More are better.)
- [x] I built this PR locally for my native architecture, (ARCH-LIBC)
- [ ] I built this PR locally for these architectures (if supported. mark crossbuilds):
  - [ ] aarch64-musl
  - [ ] armv7l
  - [ ] armv6l-musl