Zulip Chat Archive

Stream: general

Topic: Farewell to mini_crush, smt2_interface, etc.

Gabriel Ebner (Feb 21 2020 at 12:42):

Did you know that there are other Lean projects aside from mathlib that are tested by the Lean CI scripts? Like https://github.com/leanprover/smt2_interface and https://github.com/leanprover/mini_crush
I'd like to remove these projects from the Lean CI. Do you care? https://github.com/leanprover-community/lean/pull/122

Gabriel Ebner (Feb 21 2020 at 12:43):

The reason I want to remove them from the CI is that the current PRs break them: https://github.com/leanprover-community/lean/pull/121

Rob Lewis (Feb 21 2020 at 12:45):

I say go ahead and remove them.

Patrick Massot (Feb 21 2020 at 12:45):

Are those smt2 and mini_crush actually usable? I got the idea they were tech demo which are not really practical.

Gabriel Ebner (Feb 21 2020 at 12:45):

I don't think anybody uses them in production. mini_crush is actually usable. The smt2_interface doesn't produce proofs.

Patrick Massot (Feb 21 2020 at 12:48):

I like the PR message at https://github.com/leanprover-community/lean/pull/122. Leo would be proud :wink:

Patrick Massot (Feb 21 2020 at 12:49):

Would it make sense to fix mini_crush and put it into mathlib?

Patrick Massot (Feb 21 2020 at 12:50):

Who wrote that originally?

Gabriel Ebner (Feb 21 2020 at 12:50):

All of them still work in 3.5.2. @Anne Baanen's PR only breaks smt2_interface. If anybody wants it in mathlib, we could certainly merge it.

Patrick Massot (Feb 21 2020 at 12:50):

I can't find a Licence file.

Gabriel Ebner (Feb 21 2020 at 12:51):

Leo. It was an example to show that we can implement Coq tactics just as easily, but faster. License is apache. (It was originally in the main lean repo.)

Patrick Massot (Feb 21 2020 at 12:57):

What kind of statements can it prove? How does it relate to finish, cc or other such things?

Gabriel Ebner (Feb 21 2020 at 13:00):

I'm not sure. It also does induction.

Patrick Massot (Feb 21 2020 at 13:06):

I'd vote for putting it into mathlib, unless there is any down-side to this.

Anne Baanen (Feb 21 2020 at 15:42):

I'm not actually sure what causes the build failures. One looks more like a network connection timeout, and the other seems to work on my machine...

Gabriel Ebner (Feb 21 2020 at 15:55):

@Anne Baanen Look closely at the placement of the double quotes.

Anne Baanen (Feb 21 2020 at 15:59):

I don't understand which double quotes you refer to?

Gabriel Ebner (Feb 21 2020 at 16:01):

https://github.com/leanprover-community/mathlib/commit/e50512b4f446d928c6911f0dfd49f26ff5801c25

Anne Baanen (Feb 21 2020 at 16:04):

I think you are referring to uploading mathlib to azure. I'm referring to smt2_interface failing to build in my PR

Anne Baanen (Feb 21 2020 at 16:04):

There shouldn't be any SAS token needed to compile Lean, right?

Gabriel Ebner (Feb 21 2020 at 16:05):

PLEASE NO BUILD RESTARTING ON THE LEAN REPOSITORY!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

Gabriel Ebner (Feb 21 2020 at 16:06):

Seriously, travis is at capacity. Every commit takes two hours. Please commit responsibly.

Gabriel Ebner (Feb 21 2020 at 16:55):

That was maybe a bit harsh from me. I'm just trying to get these PRs merged and I'm annoyed that I have to wait even more..

Gabriel Ebner (Feb 21 2020 at 16:55):

@Anne Baanen Do I understand you correctly? The tests in smt2_interface work for you in your branch?

Last updated: Dec 20 2023 at 11:08 UTC