Polyrith error 520

Stream: mathlib4

[Bhavik Mehta]

Currently polyrith is giving error 520 from sagecell. This seems to be caused by an error on the sagecell service, which you can check here: https://sagecell.sagemath.org/service. The sagecell online version seems to still be working fine, and seemingly this should resolve itself when the sagecell web server gets fixed, but I'm mentioning it here in case other people run into this and don't understand what's happening.

[Michał Mrugała]

I just want to bump this thread since I'm still running into the issue

[Kenny Lau]

wait... mathlib4 calls an online service?

[Andrew Yang]

Given the sage service has been down for now for a month now, I think it is safe to say that it will not go back on in the near future. So it would be nice if polyrith can support local installations.

[Andrew Yang]

Kenny Lau said:

wait... mathlib4 calls an online service?

It can, and polyrith is currently the only one that does.

[Kenny Lau]

and after the calling is the result converted back to an independent proof?

[Riccardo Brasca]

Kenny Lau said:

and after the calling is the result converted back to an independent proof?

Yes

[Kenny Lau]

as in, you actually replace the code with one that is independent?

[Kenny Lau]

similar to how simp? replaces itself when you click on the message

[Aaron Liu]

Sage figures out a combination of hypotheses that equals the goal, and polyrith converts this into a call to the linear_combination tactic.

[Kenny Lau]

ok, good, lean is still sound then

[Andrew Yang]

Are you sure? Have you formalized the whole GMP :wink:

[Kenny Lau]

let's formalise lean inside lean

[Michał Mrugała]

Mario is already doing that

[Aaron Liu]

https://github.com/digama0/lean4lean

[Bhavik Mehta]

Andrew Yang said:

Given the sage service has been down for now for a month now, I think it is safe to say that it will not go back on in the near future. So it would be nice if polyrith can support local installations.

It may be the case that the sagecell service isn't really used, and so the sage people aren't aware of this... Or alternatively, the endpoint has changed

[Jz Pan]

Andrew Yang said:

Kenny Lau said:

wait... mathlib4 calls an online service?

It can, and polyrith is currently the only one that does.

There are also #search I think.

[Matthias Köppe]

Andrew Yang said:

it would be nice if polyrith can support local installations.

A full local installation of Sage will likely not be necessary for this. https://pypi.org/project/passagemath-singular/

[Thomas Zhu]

Hopefully grind can become a drop-in replacement for polyrith in most cases

[Kevin Buzzard]

@William Stein are you aware of this?

[Bhavik Mehta]

Thomas Zhu said:

Hopefully grind can become a drop-in replacement for polyrith in most cases

Yes, but I would like to have other tactics (some of which are written, and led me to discover the problem at the start of this thread, it wasn't polyrith!) which use the sage server

[William Stein]

My understanding is that the sage cell server is working. It is monitored, and there are many complaints when it goes down. I guess I don't understand what "Given the sage service has been down for now for a month now" means. Perhaps it means that something changed with the https://sagecell.sagemath.org/ to make it incompatible with something else. In that case, I have no opinion, because I'm not aware of the issue.

[Julian Berman]

I see the same as what the original message reported -- https://sagecell.sagemath.org/ seems to work fine, but https://sagecell.sagemath.org/service does not and returns a 520 error page from Cloudflare in a browser, and similarly if one tries it via Python including via https://github.com/sagemath/sagecell/blob/master/contrib/sagecell-client/sagecell-service.py which looks like a little script to test the endpoint.

[Julian Berman]

The page gives an email address (for Andrey Novoseltsev) who I just passed the message along to (even though I know who William is :).

[Julian Berman]

Andrey responded already, to say:

It is down due to overuse by somebody, maybe Lean users. It is not going to come back on public servers, but interested people are welcome to spin off their own servers!

So it sounds like unfortunately it's going to stay offline.

[Thomas Zhu]

Overuse caused by LLM training sounds very plausible

[Kim Morrison]

I wonder if there is an easy way to prove to a remote server that you are running Lean. :-)

[Kim Morrison]

Have the server issue a challenge problem that Lean's automation can reliably solve, then have the server verify the proof?

[Bhavik Mehta]

This isn't quite proof, but polyrith currently does let the server know that it's coming from Lean: https://github.com/leanprover-community/mathlib4/blob/7deb334c5f5104f4edad1a6396dd02a8cddefb86/Mathlib/Tactic/Polyrith.lean#L330 and https://github.com/leanprover-community/mathlib4/blob/7deb334c5f5104f4edad1a6396dd02a8cddefb86/Mathlib/Tactic/Polyrith.lean#L350

[Robin Carlier]

In the meantime, maybe it could be a good idea to make it so that users can override the default URL hardcoded in the tactic (an env var or a set_optionis a good way to achieve this?), so that if someone wants to set up a server locally (or if someone sets up a server for lean users) and want to use their own server for their polyrith usage it’s an option.

[Matthias Köppe]

Perhaps a good opportunity to dust off @Miguel Marco's PR https://github.com/leanprover-community/mathlib4/pull/20334

[Rob Lewis]

I didn't see this thread/issue until now -- please feel free to tag me on polyrith-related issues!

Julian Berman said:

Andrey responded already, to say:

It is down due to overuse by somebody, maybe Lean users. It is not going to come back on public servers, but interested people are welcome to spin off their own servers!

So it sounds like unfortunately it's going to stay offline.

We've reached an (unfortunate) milestone. Three years ago I asked Andrey for permission to hook up polyrith to SageCell and his answer was

I am glad that our service was useful to you! From what you are describing, there are no issues with using the public servers. There are health checks that run simple computations every couple of minutes, so 720 times a day, actually 2000 over 3 containers. I don't anticipate problems with actual users either, and if you do manage to become so popular - it would be a great opportunity indeed to setup another server!

So I guess we've gone beyond "so popular"...

[Rob Lewis]

My understanding is that there will be (or already is?) a Grobner basis module in core Lean. @Kim Morrison do you know details?

[Rob Lewis]

Long term, using an internal implementation is going to be the most stable solution

[Rob Lewis]

I don't think it's sustainable to expect users to have a local install of Sage or anything else besides Lean

[Matthias Köppe]

Are there other tactics that use a locally installed Python? Elsewhere I saw cvc5 (a SAT/SMT solver) mentioned
(edit: That may have been https://github.com/ufmg-smite/lean-smt, https://github.com/abdoo8080/lean-cvc5)

[Rob Lewis]

I believe polyrith is the only mathlib tactic that calls an external tool

[Jireh Loreaux]

@Rob Lewis , but there's this from above:
Bhavik Mehta said:

Yes, but I would like to have other tactics (some of which are written, and led me to discover the problem at the start of this thread, it wasn't polyrith!) which use the sage server

[Matthias Köppe]

If there is interest, I can help on the Sage side of things, for example by preparing a lightweight version of the SageCell server that can run locally without a full installation of Sage, https://github.com/passagemath/passagemath/issues/1058

[Rob Lewis]

A lightweight local SageCell would be extremely helpful, especially if it's possible to occasionally update how much it imports. I've looked at the normal SageCell installation directions and I don't see myself getting a server up and running anytime soon.

[Matthias Köppe]

I've created the fork https://github.com/passagemath/passagemath-cell-server for this work

[Matthias Köppe]

@Rob Lewis I've got it to the point that it can be installed with a simple "pip install", see updated README. The next step should probably be to cut out the ssh-based connection to work servers.

[Kim Morrison]

Rob Lewis said:

My understanding is that there will be (or already is?) a Grobner basis module in core Lean. Kim Morrison do you know details?

There's some documentation about the Grobner basis solver at https://pr-451--lean-reference-manual-review.netlify.app/The--grind--tactic/Algebraic-Solver-_LPAR_Commutative-Rings___-Fields_RPAR_/#The-Lean-Language-Reference--The--grind--tactic--Algebraic-Solver-_LPAR_Commutative-Rings___-Fields_RPAR_.

Hopefully available on Tuesday or Wednesday.

[Rob Lewis]

@Matthias Köppe thanks for this. I'm trying to follow the directions in the readme, but getting errors at sage -sh -c make:

ERROR in ./js/css.js
Module not found: Error: Can't resolve 'colorpicker.css' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/css.js
Module not found: Error: Can't resolve 'fontawesome.css' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/css.js
Module not found: Error: Can't resolve 'sagecell.css' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/interact_cell.js
Module not found: Error: Can't resolve 'base/js/events' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/session.js
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/session.js
Module not found: Error: Can't resolve 'base/js/events' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/session.js
Module not found: Error: Can't resolve 'base/js/namespace' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/session.js
Module not found: Error: Can't resolve 'services/kernels/kernel' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/utils.js
Module not found: Error: Can't resolve 'base/js/utils' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/cell.js
 @ ./js/main.js

ERROR in ./js/widgets.js
Module not found: Error: Can't resolve 'mpl' in '/home/rlewis13/lean/passagemath-cell-server/js'
 @ ./js/session.js
 @ ./js/cell.js
 @ ./js/main.js

[Matthias Köppe]

@Rob Lewis Thanks for testing, fixed now