Github messages for voidlinux
 help / color / mirror / Atom feed
* [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0
@ 2022-03-01 16:20 tornaria
  2022-03-01 16:24 ` tornaria
                   ` (12 more replies)
  0 siblings, 13 replies; 14+ messages in thread
From: tornaria @ 2022-03-01 16:20 UTC (permalink / raw)
  To: ml

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

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

https://github.com/tornaria/void-packages lean-community
https://github.com/void-linux/void-packages/pull/35907

[Help with cmake needed] New package: lean-community-3.40.0
This is an updated version of #32559.

Recently (maybe a cmake update) there is a test failure that seems to be related to cmake. Here's the relevant part of the output of `./xbps-src check lean-community`:
```
[0/1] Running tests...
Test project /builddir/lean-3.40.0/src/build
          Start    1: style_check
   1/1427 Test    #1: style_check .................................................***Failed   26.22 sec
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:50:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:54:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:130:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:139:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:149:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:154:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:291:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:313:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:670:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:675:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:681:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:688:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:689:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:690:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:699:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:704:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:710:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:768:  { should almost always be at the end of the previous line  [whitespace/braces] [4]
/builddir/lean-3.40.0/src/build/githash.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/version.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
Total errors found: 21
```

This may be related to the following warning that is output by `./xbps-src configure lean-community`:
```
CMake Warning (dev):
  Policy CMP0058 is not set: Ninja requires custom command byproducts to be
  explicit.  Run "cmake --help-policy CMP0058" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

  This project specifies custom command DEPENDS on files in the build tree
  that are not specified as the OUTPUT or BYPRODUCTS of any
  add_custom_command or add_custom_target:

   CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp

  For compatibility with versions of CMake that did not have the BYPRODUCTS
  option, CMake is generating phony rules for such files to convince 'ninja'
  to build.

  Project authors should add the missing BYPRODUCTS or OUTPUT options to the
  custom commands that produce these files.
This warning is for project developers.  Use -Wno-dev to suppress it.
```

Any help with this is appreciated. I'm sure this was working ok recently.

Another issue is a test failing on i686 only (cf https://github.com/leanprover-community/lean/issues/685) is there an easy way to disable a particular test for i686?

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

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

From 78117fb96d1802318b3dbd141a8eb74874777505 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gonzalo=20Tornar=C3=ADa?= <tornaria@cmat.edu.uy>
Date: Tue, 1 Mar 2022 12:58:43 -0300
Subject: [PATCH] New package: lean-community-3.40.0

---
 srcpkgs/lean-community/template | 21 +++++++++++++++++++++
 1 file changed, 21 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..1ff836ce7dea
--- /dev/null
+++ b/srcpkgs/lean-community/template
@@ -0,0 +1,21 @@
+# Template file for 'lean-community'
+pkgname=lean-community
+version=3.40.0
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+configure_args="-DUSE_GITHASH=OFF"
+hostmakedepends="python3"
+makedepends="gmp-devel"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Gonzalo Tornaría <tornaria@cmat.edu.uy>"
+license="Apache-2.0"
+homepage="https://leanprover-community.github.io/"
+changelog="https://raw.githubusercontent.com/leanprover-community/lean/master/doc/changes.md"
+distfiles="https://github.com/leanprover-community/lean/archive/v${version}.tar.gz"
+checksum=955496d97b2193fea3609a3f3f7ad9cab6413e0d0ea6c1a03d6c1656a2ec08ef
+
+if [ -n "$CROSS_BUILD" ]; then
+	configure_args+=" -DCROSS_COMPILE=ON"
+fi

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [Help with cmake needed] New package: lean-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
@ 2022-03-01 16:24 ` tornaria
  2022-03-01 16:26 ` leahneukirchen
                   ` (11 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: tornaria @ 2022-03-01 16:24 UTC (permalink / raw)
  To: ml

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

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1055621052

Comment:
cc @eloitor

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [Help with cmake needed] New package: lean-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
  2022-03-01 16:24 ` tornaria
@ 2022-03-01 16:26 ` leahneukirchen
  2022-03-01 16:30 ` leahneukirchen
                   ` (10 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: leahneukirchen @ 2022-03-01 16:26 UTC (permalink / raw)
  To: ml

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

New comment by leahneukirchen on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1055622224

Comment:
Please name this lean3-community, as lean3 and lean4 will coexist for forseeable future.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [Help with cmake needed] New package: lean-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
  2022-03-01 16:24 ` tornaria
  2022-03-01 16:26 ` leahneukirchen
@ 2022-03-01 16:30 ` leahneukirchen
  2022-03-01 18:13 ` [PR PATCH] [Updated] " tornaria
                   ` (9 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: leahneukirchen @ 2022-03-01 16:30 UTC (permalink / raw)
  To: ml

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

New comment by leahneukirchen on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1055626966

Comment:
Just patch out buggy tests, we don't need to check upstream coding conventions for our builds.

The one you found on i686 looks like a real bug at first, however. Can you reproduce that in a LSP editor?

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [PR PATCH] [Updated] [Help with cmake needed] New package: lean-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (2 preceding siblings ...)
  2022-03-01 16:30 ` leahneukirchen
@ 2022-03-01 18:13 ` tornaria
  2022-03-01 18:25 ` tornaria
                   ` (8 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: tornaria @ 2022-03-01 18:13 UTC (permalink / raw)
  To: ml

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

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

https://github.com/tornaria/void-packages lean-community
https://github.com/void-linux/void-packages/pull/35907

[Help with cmake needed] New package: lean-community-3.40.0
This is an updated version of #32559.

Recently (maybe a cmake update) there is a test failure that seems to be related to cmake. Here's the relevant part of the output of `./xbps-src check lean-community`:
```
[0/1] Running tests...
Test project /builddir/lean-3.40.0/src/build
          Start    1: style_check
   1/1427 Test    #1: style_check .................................................***Failed   26.22 sec
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:50:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:54:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:130:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:139:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:149:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:154:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:291:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:313:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:670:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:675:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:681:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:688:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:689:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:690:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:699:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:704:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:710:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:768:  { should almost always be at the end of the previous line  [whitespace/braces] [4]
/builddir/lean-3.40.0/src/build/githash.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/version.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
Total errors found: 21
```

This may be related to the following warning that is output by `./xbps-src configure lean-community`:
```
CMake Warning (dev):
  Policy CMP0058 is not set: Ninja requires custom command byproducts to be
  explicit.  Run "cmake --help-policy CMP0058" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

  This project specifies custom command DEPENDS on files in the build tree
  that are not specified as the OUTPUT or BYPRODUCTS of any
  add_custom_command or add_custom_target:

   CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp

  For compatibility with versions of CMake that did not have the BYPRODUCTS
  option, CMake is generating phony rules for such files to convince 'ninja'
  to build.

  Project authors should add the missing BYPRODUCTS or OUTPUT options to the
  custom commands that produce these files.
This warning is for project developers.  Use -Wno-dev to suppress it.
```

Any help with this is appreciated. I'm sure this was working ok recently.

Another issue is a test failing on i686 only (cf https://github.com/leanprover-community/lean/issues/685) is there an easy way to disable a particular test for i686?

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

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

From ea74c88e0d3c31b86015d9cc3d6178c97bb10a93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gonzalo=20Tornar=C3=ADa?= <tornaria@cmat.edu.uy>
Date: Tue, 1 Mar 2022 12:58:43 -0300
Subject: [PATCH] New package: lean3-community-3.40.0

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

diff --git a/srcpkgs/lean3-community/template b/srcpkgs/lean3-community/template
new file mode 100644
index 000000000000..ee03962f5ee3
--- /dev/null
+++ b/srcpkgs/lean3-community/template
@@ -0,0 +1,31 @@
+# Template file for 'lean3-community'
+pkgname=lean3-community
+version=3.40.0
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+configure_args="-DUSE_GITHASH=OFF"
+hostmakedepends="python3"
+makedepends="gmp-devel"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Gonzalo Tornaría <tornaria@cmat.edu.uy>"
+license="Apache-2.0"
+homepage="https://leanprover-community.github.io/"
+changelog="https://raw.githubusercontent.com/leanprover-community/lean/master/doc/changes.md"
+distfiles="https://github.com/leanprover-community/lean/archive/v${version}.tar.gz"
+checksum=955496d97b2193fea3609a3f3f7ad9cab6413e0d0ea6c1a03d6c1656a2ec08ef
+
+if [ -n "$CROSS_BUILD" ]; then
+	configure_args+=" -DCROSS_COMPILE=ON"
+fi
+
+do_check() {
+	cd ${cmake_builddir:=build}
+	# style_check: fails on (generated file)
+	#	CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp
+	#   See: https://github.com/void-linux/void-packages/pull/35907
+	# complete_trailing_period: fails on i686
+	#	See: https://github.com/leanprover-community/lean/issues/685
+	ctest -E 'style_check|complete_trailing_period'
+}

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [Help with cmake needed] New package: lean-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (3 preceding siblings ...)
  2022-03-01 18:13 ` [PR PATCH] [Updated] " tornaria
@ 2022-03-01 18:25 ` tornaria
  2022-03-08 11:39 ` New package: lean3-community-3.40.0 ram02z
                   ` (7 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: tornaria @ 2022-03-01 18:25 UTC (permalink / raw)
  To: ml

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

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1055730991

Comment:
 > Just patch out buggy tests, we don't need to check upstream coding conventions for our builds.

That was not obvious. I had to rewrite `do_check()` to use `ctest -E <regex>`. The build-style uses `ninja test` for this, but I didn't see a way to pass options to `ctest`.

I wish xbps-src had some tools to make skipping tests by name easier for the standard test frameworks (cmake, autotools, pytest, etc).

> The one you found on i686 looks like a real bug at first, however. Can you reproduce that in a LSP editor?

I've just disabled since I don't want to worry about 32 bit right now.

TBH, I don't yet know how to actually USE lean locally -- I want to learn lean so I've been playing with some of the tutorials using the online version. I don't have a clue how to move forward with this. Apparently I need more stuff, like `leanproject` to install mathlib, etc. And I take that this cannot be run from CLI, I need some sort of plugin (unfortunately, it seems there is no vim plugin, only a neovim one).

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (4 preceding siblings ...)
  2022-03-01 18:25 ` tornaria
@ 2022-03-08 11:39 ` ram02z
  2022-05-10  1:26 ` [PR PATCH] [Updated] " tornaria
                   ` (6 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: ram02z @ 2022-03-08 11:39 UTC (permalink / raw)
  To: ml

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

New comment by ram02z on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1061688653

Comment:
>  Apparently I need more stuff, like `leanproject` to install mathlib, etc.

I have packaged mathlib-tools (https://github.com/void-linux/void-packages/pull/33587). It contains leanproject, which will update mathlib per project.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [PR PATCH] [Updated] New package: lean3-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (5 preceding siblings ...)
  2022-03-08 11:39 ` New package: lean3-community-3.40.0 ram02z
@ 2022-05-10  1:26 ` tornaria
  2022-05-10  2:57 ` tornaria
                   ` (5 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: tornaria @ 2022-05-10  1:26 UTC (permalink / raw)
  To: ml

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

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

https://github.com/tornaria/void-packages lean-community
https://github.com/void-linux/void-packages/pull/35907

New package: lean3-community-3.40.0
This is an updated version of #32559.

Recently (maybe a cmake update) there is a test failure that seems to be related to cmake. Here's the relevant part of the output of `./xbps-src check lean-community`:
```
[0/1] Running tests...
Test project /builddir/lean-3.40.0/src/build
          Start    1: style_check
   1/1427 Test    #1: style_check .................................................***Failed   26.22 sec
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:50:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:54:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:130:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:139:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:149:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:154:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:291:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:313:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:670:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:675:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:681:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:688:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:689:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:690:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:699:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:704:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:710:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:768:  { should almost always be at the end of the previous line  [whitespace/braces] [4]
/builddir/lean-3.40.0/src/build/githash.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/version.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
Total errors found: 21
```

This may be related to the following warning that is output by `./xbps-src configure lean-community`:
```
CMake Warning (dev):
  Policy CMP0058 is not set: Ninja requires custom command byproducts to be
  explicit.  Run "cmake --help-policy CMP0058" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

  This project specifies custom command DEPENDS on files in the build tree
  that are not specified as the OUTPUT or BYPRODUCTS of any
  add_custom_command or add_custom_target:

   CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp

  For compatibility with versions of CMake that did not have the BYPRODUCTS
  option, CMake is generating phony rules for such files to convince 'ninja'
  to build.

  Project authors should add the missing BYPRODUCTS or OUTPUT options to the
  custom commands that produce these files.
This warning is for project developers.  Use -Wno-dev to suppress it.
```

Any help with this is appreciated. I'm sure this was working ok recently.

Another issue is a test failing on i686 only (cf https://github.com/leanprover-community/lean/issues/685) is there an easy way to disable a particular test for i686?

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

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

From 4a4a0eabbc8828ae2491e8836125c35573a26398 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gonzalo=20Tornar=C3=ADa?= <tornaria@cmat.edu.uy>
Date: Tue, 1 Mar 2022 12:58:43 -0300
Subject: [PATCH 1/2] New package: lean3-community-3.40.0

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

diff --git a/srcpkgs/lean3-community/template b/srcpkgs/lean3-community/template
new file mode 100644
index 000000000000..ee03962f5ee3
--- /dev/null
+++ b/srcpkgs/lean3-community/template
@@ -0,0 +1,31 @@
+# Template file for 'lean3-community'
+pkgname=lean3-community
+version=3.40.0
+revision=1
+wrksrc="lean-$version"
+build_wrksrc=src
+build_style=cmake
+configure_args="-DUSE_GITHASH=OFF"
+hostmakedepends="python3"
+makedepends="gmp-devel"
+short_desc="Lean Theorem Prover, maintained by the Lean community"
+maintainer="Gonzalo Tornaría <tornaria@cmat.edu.uy>"
+license="Apache-2.0"
+homepage="https://leanprover-community.github.io/"
+changelog="https://raw.githubusercontent.com/leanprover-community/lean/master/doc/changes.md"
+distfiles="https://github.com/leanprover-community/lean/archive/v${version}.tar.gz"
+checksum=955496d97b2193fea3609a3f3f7ad9cab6413e0d0ea6c1a03d6c1656a2ec08ef
+
+if [ -n "$CROSS_BUILD" ]; then
+	configure_args+=" -DCROSS_COMPILE=ON"
+fi
+
+do_check() {
+	cd ${cmake_builddir:=build}
+	# style_check: fails on (generated file)
+	#	CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp
+	#   See: https://github.com/void-linux/void-packages/pull/35907
+	# complete_trailing_period: fails on i686
+	#	See: https://github.com/leanprover-community/lean/issues/685
+	ctest -E 'style_check|complete_trailing_period'
+}

From 77889c1422eb7366a651e0fca62b3cac8e72b289 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gonzalo=20Tornar=C3=ADa?= <tornaria@cmat.edu.uy>
Date: Mon, 9 May 2022 22:13:05 -0300
Subject: [PATCH 2/2] lean3-community: update to 3.42.1.

---
 srcpkgs/lean3-community/template | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/srcpkgs/lean3-community/template b/srcpkgs/lean3-community/template
index ee03962f5ee3..7ca58b1bf52d 100644
--- a/srcpkgs/lean3-community/template
+++ b/srcpkgs/lean3-community/template
@@ -1,6 +1,6 @@
 # Template file for 'lean3-community'
 pkgname=lean3-community
-version=3.40.0
+version=3.42.1
 revision=1
 wrksrc="lean-$version"
 build_wrksrc=src
@@ -14,7 +14,8 @@ license="Apache-2.0"
 homepage="https://leanprover-community.github.io/"
 changelog="https://raw.githubusercontent.com/leanprover-community/lean/master/doc/changes.md"
 distfiles="https://github.com/leanprover-community/lean/archive/v${version}.tar.gz"
-checksum=955496d97b2193fea3609a3f3f7ad9cab6413e0d0ea6c1a03d6c1656a2ec08ef
+checksum=5b8cbfdea6cf4de5488467297958876aa0b3a79ed5806f7d0f01a0c396beb4e2
+nocross=yes # runs binaries built for target (TODO)
 
 if [ -n "$CROSS_BUILD" ]; then
 	configure_args+=" -DCROSS_COMPILE=ON"
@@ -27,5 +28,5 @@ do_check() {
 	#   See: https://github.com/void-linux/void-packages/pull/35907
 	# complete_trailing_period: fails on i686
 	#	See: https://github.com/leanprover-community/lean/issues/685
-	ctest -E 'style_check|complete_trailing_period'
+	ctest -E 'style_check|complete_trailing_period' ${makejobs}
 }

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.40.0
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (6 preceding siblings ...)
  2022-05-10  1:26 ` [PR PATCH] [Updated] " tornaria
@ 2022-05-10  2:57 ` tornaria
  2022-05-27 21:01 ` New package: lean3-community-3.42.1 Eloitor
                   ` (4 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: tornaria @ 2022-05-10  2:57 UTC (permalink / raw)
  To: ml

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

New comment by tornaria on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1121832833

Comment:
On x86_64-musl:
```
The following tests FAILED:
	492 - leanruntest_all (Timeout)
	639 - leanruntest_async_map.lean (Failed)
```

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.42.1
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (7 preceding siblings ...)
  2022-05-10  2:57 ` tornaria
@ 2022-05-27 21:01 ` Eloitor
  2022-08-29  2:14 ` github-actions
                   ` (3 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: Eloitor @ 2022-05-27 21:01 UTC (permalink / raw)
  To: ml

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

New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1140037684

Comment:
Maybe we should package https://github.com/leanprover/elan too... Different lean projects require different versions of lean, and `elan` ensures you use the correct version with each project.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.42.1
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (8 preceding siblings ...)
  2022-05-27 21:01 ` New package: lean3-community-3.42.1 Eloitor
@ 2022-08-29  2:14 ` github-actions
  2022-09-12  2:15 ` [PR PATCH] [Closed]: " github-actions
                   ` (2 subsequent siblings)
  12 siblings, 0 replies; 14+ messages in thread
From: github-actions @ 2022-08-29  2:14 UTC (permalink / raw)
  To: ml

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

New comment by github-actions[bot] on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1229666468

Comment:
Pull Requests become stale 90 days after last activity and are closed 14 days after that.  If this pull request is still relevant bump it or assign it.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: [PR PATCH] [Closed]: New package: lean3-community-3.42.1
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (9 preceding siblings ...)
  2022-08-29  2:14 ` github-actions
@ 2022-09-12  2:15 ` github-actions
  2022-11-17  8:28 ` Eloitor
  2022-11-17 10:18 ` Eloitor
  12 siblings, 0 replies; 14+ messages in thread
From: github-actions @ 2022-09-12  2:15 UTC (permalink / raw)
  To: ml

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

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

New package: lean3-community-3.42.1
https://github.com/void-linux/void-packages/pull/35907

Description:
This is an updated version of #32559.

Recently (maybe a cmake update) there is a test failure that seems to be related to cmake. Here's the relevant part of the output of `./xbps-src check lean-community`:
```
[0/1] Running tests...
Test project /builddir/lean-3.40.0/src/build
          Start    1: style_check
   1/1427 Test    #1: style_check .................................................***Failed   26.22 sec
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:50:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:54:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:130:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:139:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:149:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:154:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:291:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:313:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:670:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:675:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:681:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:688:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:689:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:690:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:699:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:704:  Weird number of spaces at line-start.  Are you using a 2-space indent?  [whitespace/indent] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:710:  Missing space after ,  [whitespace/comma] [3]
/builddir/lean-3.40.0/src/build/CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp:768:  { should almost always be at the end of the previous line  [whitespace/braces] [4]
/builddir/lean-3.40.0/src/build/githash.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
/builddir/lean-3.40.0/src/build/version.h:0:  No copyright message found.  You should have a line: "Copyright [year] <Copyright Owner>"  [legal/copyright] [5]
Total errors found: 21
```

This may be related to the following warning that is output by `./xbps-src configure lean-community`:
```
CMake Warning (dev):
  Policy CMP0058 is not set: Ninja requires custom command byproducts to be
  explicit.  Run "cmake --help-policy CMP0058" for policy details.  Use the
  cmake_policy command to set the policy and suppress this warning.

  This project specifies custom command DEPENDS on files in the build tree
  that are not specified as the OUTPUT or BYPRODUCTS of any
  add_custom_command or add_custom_target:

   CMakeFiles/3.22.2/CompilerIdCXX/CMakeCXXCompilerId.cpp

  For compatibility with versions of CMake that did not have the BYPRODUCTS
  option, CMake is generating phony rules for such files to convince 'ninja'
  to build.

  Project authors should add the missing BYPRODUCTS or OUTPUT options to the
  custom commands that produce these files.
This warning is for project developers.  Use -Wno-dev to suppress it.
```

Any help with this is appreciated. I'm sure this was working ok recently.

Another issue is a test failing on i686 only (cf https://github.com/leanprover-community/lean/issues/685) is there an easy way to disable a particular test for i686?

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.42.1
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (10 preceding siblings ...)
  2022-09-12  2:15 ` [PR PATCH] [Closed]: " github-actions
@ 2022-11-17  8:28 ` Eloitor
  2022-11-17 10:18 ` Eloitor
  12 siblings, 0 replies; 14+ messages in thread
From: Eloitor @ 2022-11-17  8:28 UTC (permalink / raw)
  To: ml

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

New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1318265979

Comment:
I updated the template to 3.49.0 and now there is only one test that fails due to a timeout in my old computer. Maybe the CI build does not have this timeout. Maybe we can disable the timeout or remove this test... Which option is best?
 
```
495/1438 Test  #493: leantest_wrong_arity.lean ...................................   Passed    0.01 sec
          Start  495: leanruntest_all
 496/1438 Test  #495: leanruntest_all .............................................***Timeout 1500.12 sec
connect
recv
[S, E, C, R, E, T, _, D, A, T, A]

          Start  496: leanruntest_1010.lean
 497/1438 Test  #496: leanruntest_1010.lean .......................................   Passed    3.10 sec
          Start  497: leanruntest_1089.lean

[ more output ]


99% tests passed, 1 tests failed out of 1438

Total Test time (real) = 4973.43 sec

The following tests FAILED:
	495 - leanruntest_all (Timeout)
Errors while running CTest
```

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: New package: lean3-community-3.42.1
  2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
                   ` (11 preceding siblings ...)
  2022-11-17  8:28 ` Eloitor
@ 2022-11-17 10:18 ` Eloitor
  12 siblings, 0 replies; 14+ messages in thread
From: Eloitor @ 2022-11-17 10:18 UTC (permalink / raw)
  To: ml

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

New comment by Eloitor on void-packages repository

https://github.com/void-linux/void-packages/pull/35907#issuecomment-1318265979

Comment:
I updated the template to 3.49.0 and now there is only one test that fails due to a timeout in my old computer.
 
```
495/1438 Test  #493: leantest_wrong_arity.lean ...................................   Passed    0.01 sec
          Start  495: leanruntest_all
 496/1438 Test  #495: leanruntest_all .............................................***Timeout 1500.12 sec
connect
recv
[S, E, C, R, E, T, _, D, A, T, A]

          Start  496: leanruntest_1010.lean
 497/1438 Test  #496: leanruntest_1010.lean .......................................   Passed    3.10 sec
          Start  497: leanruntest_1089.lean

[ more output ]


99% tests passed, 1 tests failed out of 1438

Total Test time (real) = 4973.43 sec

The following tests FAILED:
	495 - leanruntest_all (Timeout)
Errors while running CTest
```

Update: I tried again in a faster machine and it now builds successfully. The test that failed before now runs in 84 sec, I think I didn't add the patches to the template. 

@tornaria should I open a new PR?

^ permalink raw reply	[flat|nested] 14+ messages in thread

end of thread, other threads:[~2022-11-17 10:18 UTC | newest]

Thread overview: 14+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-03-01 16:20 [PR PATCH] [Help with cmake needed] New package: lean-community-3.40.0 tornaria
2022-03-01 16:24 ` tornaria
2022-03-01 16:26 ` leahneukirchen
2022-03-01 16:30 ` leahneukirchen
2022-03-01 18:13 ` [PR PATCH] [Updated] " tornaria
2022-03-01 18:25 ` tornaria
2022-03-08 11:39 ` New package: lean3-community-3.40.0 ram02z
2022-05-10  1:26 ` [PR PATCH] [Updated] " tornaria
2022-05-10  2:57 ` tornaria
2022-05-27 21:01 ` New package: lean3-community-3.42.1 Eloitor
2022-08-29  2:14 ` github-actions
2022-09-12  2:15 ` [PR PATCH] [Closed]: " github-actions
2022-11-17  8:28 ` Eloitor
2022-11-17 10:18 ` Eloitor

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).