Commit 2025-01-26 16:12 a1037826

View on Github →

chore(Tactic/Polyrith): remove polyrith dependency on Python (#17626)

Removed dependency on Python to make requests to SageMath, using curl instead
Moved API calling logic from scripts/polyrith_sage.py to Tactic/Polyrith.lean
Moved scripts/polyrith_sage_helper.py inline

Estimated changes

Modified Mathlib/Tactic/Polyrith.lean

deleted def Mathlib.Tactic.Polyrith.createSageArgs

modified def Mathlib.Tactic.Polyrith.parseContext

added def Mathlib.Tactic.Polyrith.runSage

added def Mathlib.Tactic.Polyrith.sageCreateQuery

added def Mathlib.Tactic.Polyrith.sageHelperFunctions

deleted def Mathlib.Tactic.Polyrith.sageOutput

added def Mathlib.Tactic.Polyrith.sageTypeStr

Modified MathlibTest/polyrith.lean

Deleted scripts/polyrith_sage.py

Modified scripts/polyrith_sage_helper.py