* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
@ 2021-08-17 21:48 ` Eloitor
2021-08-18 3:24 ` Eloitor
` (14 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-17 21:48 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
2021-08-17 21:48 ` [PR PATCH] [Updated] " Eloitor
@ 2021-08-18 3:24 ` Eloitor
2021-08-19 21:58 ` [PR REVIEW] " tornaria
` (13 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-18 3:24 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR REVIEW] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
2021-08-17 21:48 ` [PR PATCH] [Updated] " Eloitor
2021-08-18 3:24 ` Eloitor
@ 2021-08-19 21:58 ` tornaria
2021-08-19 22:02 ` [PR PATCH] [Updated] " Eloitor
` (12 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2021-08-19 21:58 UTC (permalink / raw)
To: ml
[-- 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.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (2 preceding siblings ...)
2021-08-19 21:58 ` [PR REVIEW] " tornaria
@ 2021-08-19 22:02 ` Eloitor
2021-08-19 22:02 ` [PR REVIEW] " Eloitor
` (11 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-19 22:02 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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"
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR REVIEW] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (3 preceding siblings ...)
2021-08-19 22:02 ` [PR PATCH] [Updated] " Eloitor
@ 2021-08-19 22:02 ` Eloitor
2021-08-19 22:32 ` tornaria
` (10 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-19 22:02 UTC (permalink / raw)
To: ml
[-- 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.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (4 preceding siblings ...)
2021-08-19 22:02 ` [PR REVIEW] " Eloitor
@ 2021-08-19 22:32 ` tornaria
2021-08-19 22:37 ` tornaria
` (9 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2021-08-19 22:32 UTC (permalink / raw)
To: ml
[-- 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?
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (5 preceding siblings ...)
2021-08-19 22:32 ` tornaria
@ 2021-08-19 22:37 ` tornaria
2021-08-20 6:44 ` [PR PATCH] [Updated] " Eloitor
` (8 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2021-08-19 22:37 UTC (permalink / raw)
To: ml
[-- 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
```
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (6 preceding siblings ...)
2021-08-19 22:37 ` tornaria
@ 2021-08-20 6:44 ` Eloitor
2021-08-20 6:46 ` Eloitor
` (7 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-20 6:44 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (7 preceding siblings ...)
2021-08-20 6:44 ` [PR PATCH] [Updated] " Eloitor
@ 2021-08-20 6:46 ` Eloitor
2021-08-20 6:57 ` [PR PATCH] [Updated] " Eloitor
` (6 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-20 6:46 UTC (permalink / raw)
To: ml
[-- 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.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (8 preceding siblings ...)
2021-08-20 6:46 ` Eloitor
@ 2021-08-20 6:57 ` Eloitor
2021-08-20 12:25 ` tornaria
` (5 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-20 6:57 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (9 preceding siblings ...)
2021-08-20 6:57 ` [PR PATCH] [Updated] " Eloitor
@ 2021-08-20 12:25 ` tornaria
2021-08-24 11:52 ` Eloitor
` (4 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2021-08-20 12:25 UTC (permalink / raw)
To: ml
[-- 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`.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (10 preceding siblings ...)
2021-08-20 12:25 ` tornaria
@ 2021-08-24 11:52 ` Eloitor
2021-08-24 12:52 ` tornaria
` (3 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-24 11:52 UTC (permalink / raw)
To: ml
[-- 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
```
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (11 preceding siblings ...)
2021-08-24 11:52 ` Eloitor
@ 2021-08-24 12:52 ` tornaria
2021-08-25 22:30 ` [PR PATCH] [Updated] " Eloitor
` (2 subsequent siblings)
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2021-08-24 12:52 UTC (permalink / raw)
To: ml
[-- 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.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Updated] New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (12 preceding siblings ...)
2021-08-24 12:52 ` tornaria
@ 2021-08-25 22:30 ` Eloitor
2022-02-19 21:54 ` tornaria
2022-05-27 21:35 ` [PR PATCH] [Closed]: " Eloitor
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2021-08-25 22:30 UTC (permalink / raw)
To: ml
[-- 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
---
| 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 srcpkgs/lean-community/template
--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
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (13 preceding siblings ...)
2021-08-25 22:30 ` [PR PATCH] [Updated] " Eloitor
@ 2022-02-19 21:54 ` tornaria
2022-05-27 21:35 ` [PR PATCH] [Closed]: " Eloitor
15 siblings, 0 replies; 17+ messages in thread
From: tornaria @ 2022-02-19 21:54 UTC (permalink / raw)
To: ml
[-- 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.
^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [PR PATCH] [Closed]: New package: lean-community-3.32.1
2021-08-17 21:45 [PR PATCH] New package: lean-community-3.32.1 Eloitor
` (14 preceding siblings ...)
2022-02-19 21:54 ` tornaria
@ 2022-05-27 21:35 ` Eloitor
15 siblings, 0 replies; 17+ messages in thread
From: Eloitor @ 2022-05-27 21:35 UTC (permalink / raw)
To: ml
[-- 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
^ permalink raw reply [flat|nested] 17+ messages in thread