Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Towards a new SymPy

oscarbenjamin.github.io

Post reply on HN
Print view View original

11–20 of 72 posts

Re: Towards a new SymPy

#11

Post by abdullahkhalids »

StableAlkyne wrote: post #4
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.

Re: Towards a new SymPy

#12

Post by viscousviolin »

carapace wrote: post #6

Part II made the front page yesterday: https://news.ycombinator.com/item?id=37426080 A comment there makes what I think is a very good point about "the lack of consolidation of computer algebra efforts": https://news.ycombinator.com/item?id=37430437 I don't know what might drive or foster such consolidation. Maybe Category Theory? Bridging syntax?

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem.

[0] https://leanprover-community.github.io/

Re: Towards a new SymPy

#13

Post by StableAlkyne »

abdullahkhalids wrote: post #11
StableAlkyne wrote: post #4

Earlier quoted context omitted.

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.

Miniconda is faster (I prefer it, personally)...

...but Miniconda and Anaconda are the same package manager, the difference is that Anaconda comes batteries-inclused with a ton of common packages.

The reason Miniconda is faster isn't the solver, it's because it doesn't have 250 packages to go through the long checking process on.

If you have a large, complex environment in Miniconda, that environment will get slower and slower to resolve over time.

Re: Towards a new SymPy

#14

Post by scoresmoke »

StableAlkyne wrote: post #4
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Yes, this is a big disadvantage. But have you tried Mamba that aims at implementing Anaconda more efficiently? It works really well in most cases.

https://mamba.readthedocs.io/

Re: Towards a new SymPy

#15

Post by 7thaccount »

abdullahkhalids wrote: post #10
7thaccount wrote: post #5

I really liked the article and how it explained CAS vs Numerical solutions. It also looks like SymPy or SymEngine is starting to catch up to Mathematica which also is pretty cool and does the same kind of expansion of an expression into a tree of sub expressions.

Is there any comparison of their features anywhere? Last time I tried sympy a few years ago, it was quite a bit lacking compared to Mathematica.

I don't personally know, but assume it'll take many years to catch up with Mathematica which has symbolic computing as their bread and butter with a large amount of developers adding to that codebase since like the 80s.

Re: Towards a new SymPy

#16

Post by VHRanger »

abdullahkhalids wrote: post #11
StableAlkyne wrote: post #4

Earlier quoted context omitted.

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

Miniconda has a better dependency resolver, and it can resolve in less than a minute in most cases.

They have the same resolver (Conda)

You just have fewer packages installed with miniconda, so the sat problem is much smaller

Re: Towards a new SymPy

#17

Post by kzrdude »

I think banking on SymEngineX ("SEX") for the Sympy 2.0 release would be interesting branding.

I'm also cheering for Sympy, I think it's longevity now still predicts success in the future.

Re: Towards a new SymPy

#18

Post by staunton »

viscousviolin wrote: post #12
carapace wrote: post #6

Part II made the front page yesterday: https://news.ycombinator.com/item?id=37426080 A comment there makes what I think is a very good point about "the lack of consolidation of computer algebra efforts": https://news.ycombinator.com/item?id=37430437 I don't know what might drive or foster such consolidation. Maybe Category Theory? Bridging syntax?

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem. [0] https://leanprover-community.github.io/

That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).

Re: Towards a new SymPy

#19

Post by [deleted] »

StableAlkyne wrote: post #4
mathisfun123 wrote: post #3

The unfortunate thing is that core CAS functionality (and performance) should be based on a SAT/SMT engine to discover the rewrite rules and it goes without saying (but I'll say it anyway) implementing that is "hard". Naively (i.e., I haven't really thought through it), I think sympy should be built on top of z3 or cvc5 or at least very tighly integrated (e.g., support as a backend). And (again naively) I think until…

Not an expert in SAT solvers, personally. What would the benefit be in using one? Anaconda's absurdly slow dependency resolver (it takes up to 15 minutes for things Pip installs in seconds, with no way of disabling it outside of installing a third party solver) is based on SAT and left a bad taste in my mouth for them (slow, clunky, etc), but maybe it's just a poor implementation on their part.

[deleted]

Re: Towards a new SymPy

#20

Post by viscousviolin »

staunton wrote: post #18
viscousviolin wrote: post #12

Earlier quoted context omitted.

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem. [0] https://leanprover-community.github.io/

That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).

That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel.

[0] https://news.ycombinator.com/item?id=37435449

Post reply on HN