langit
commented
11 years ago In mathematica, you can execute a file by "<<file.m;". Is it possible to implement this in mathics too?
Closed langit closed 11 years ago
langit
commented
11 years ago In mathematica, you can execute a file by "<<file.m;". Is it possible to implement this in mathics too?
sn6uv
commented
11 years ago Hi @langit. This should be working already in the upcoming release:
>> << "test.m"
= 2with
$ cat test.m
#!/usr/bin/mathics
1+1This hasn't been pushed to the current stable version of mathics (0.5) running on mathics.net and available for download from mathics.org. It should work if you download mathics from this git repo.
Note: In mathematica the following is acceptable (without the quotation marks)
[1]:= << test.m
Out[1]= 2but mathics currently requires the quotation marks. Maybe we should fix this.
langit
commented
11 years ago Hi, I have hacked the main.py in mathics to run a really cool old mathematica 2.2.2 code. I still can't get everything loaded without problem, but it seems promising. Any suggestions would be highly appreciated.
sn6uv
commented
11 years ago Would you mind posting the mathematica code and any output you get?
langit
commented
11 years ago Sure, I'm glad to and thanks for taking a look at it. It is huge (maybe 100k of code in total, so I highly recommend git clone it and give it a quick run), I paste the last few lines here:
...
InequalityRules = {
(* Standard form for inequalities. *)
(a_ != b_) :> not[a == b],
(a_ > b_) :> (b < a),
(a_ >= b_) :> (b <= a),
Less[a_, b_, c__] :> and[a<b, Less[b, c]],
Greater[a_, b_, c__] :> and[a>b, Greater[b, c]],
LessEqual[a_, b_, c__] :> and[a<=b, LessEqual[b, c]],
GreaterEqual[a_, b_, c__] :> and[a>=b, GreaterEqual[b, c]],
(* Rules involving relations between 0 and a product. *)
(x_ a_ < 0) :> or[and[0 < x, a < 0], and[0 < a, x < 0]],
(x_ a_ <= 0) :> or[and[0 <= x, a <= 0], and[0 <= a, x <= 0]],
(0 < x_ a_) :> or[and[0 < x, 0 < a], and[a < 0, x < 0]],
(0 <= x_ a_) :> or[and[0 <= x, 0 <= a], and[a <= 0, x <= 0]],
(* Remove a common additive term from both sides. *)
(x_ <= y_) :> (x - y <= 0) /; x =!= 0 && y =!= 0,
(x_ < y_) :> (x - y < 0) /; x =!= 0 && y =!= 0,
(0 <= x_ + y_) :> (-x - y <= 0),
(0 < x_ + y_) :> (-x - y < 0),
(* Decide the sign of a power. *)
(0 <= a_^n_) :> True /; WeakSimplify[0<=a],
(0 < a_^n_) :> True /; WeakSimplify[0<a],
(a_^n_ <= 0) :> False /; WeakSimplify[0<a],
(a_^n_ < 0) :> False/; WeakSimplify[0<=a],
(0 < a_^n_?Negative) :> (0 < a ^ (-n)),
(0 <= a_^n_?Negative) :> (0 < a ^ (-n)),
(0 <= a_^n_) :> or[0<=a, Even[n]]/;integer[n],
(a_^n_ <= 0) :> or[a==0, and[a<0, not[Even[n]]]]/;integer[n],
(0 < a_^n_) :> or[0<a, and[a<0, Even[n]]]/;integer[n],
(a_^n_ < 0) :> and[a<0, not[Even[n]]]/;integer[n],
(* Use atomic subformula to simplify other parts of the formula. The
conditions are used to insure that the rules derived from the
subformula are not complicated and can be applied to the other parts
of the formula. *)
or[a___, b_ < c_, d___] :> or[b<c, (or[a, d] /. RulesFrom[c<=b])] /;
!TooComplicated[b<c] && appears[{a, d}, b-c],
or[a___, b_ <= c_, d___] :> or[b<=c, (or[a, d] /. RulesFrom[c<b])] /;
!TooComplicated[b<=c] && appears[{a, d}, b-c],
or[a___, b_ == c_, d___] :> or[b==c, (or[a, d] /. RulesFrom[not[c==b]])] /;
!TooComplicated[b == c] && appears[{a, d}, b-c],
and[a___, b_ < c_, d___] :> and[b<c, (and[a, d] /. RulesFrom[b<c])] /;
!TooComplicated[b<c] && appears[{a, d}, b-c],
and[a___, b_ <= c_, d___] :> and[b<=c, (and[a, d] /. RulesFrom[b<=c])] /;
!TooComplicated[b<=c] && appears[{a, d}, b-c],
and[a___, b_ == c_, d___] :> and[b==c, (and[a, d] /. RulesFrom[b==c])] /;
!TooComplicated[b==c] && appears[{a, d}, b-c],
(* Rules to decide sign of a summation. *)
(0 <= sum[f_, range_]) :> True /; WeakSimplify[0<=f],
(sum[f_, range_] <= 0) :> True /; WeakSimplify[f<=0]
};Traceback (most recent call last):
File "main.py", line 185, in
langit
commented
11 years ago How to obtain all output:
git clone git@github.com:langit/analytica.gitthen you simply run:
python main.py index.allI noticed that there are some weird complaints from Mathics:
"""
Strict/: a Strict[b] := If[TrueQ[WeakSimplify[or[a>0, a<0]]], Strict[a b], a b]; : Join[OperatorRules, AbsRule, ExpressionRules, MaxMinRules, {a == b == c :> and[a == b, b == c], a ? NumberQ == b :> b == a, a b == 0 :> or[a == 0, b == 0], a + b == c :> a + (b - c) == 0 /; c =!= 0, (x.) a == (y.) a :> or[a == 0, x == y], (x.) a ^ (n1.) == (y.) a ^ (n2.) :> or[a ^ n1 == 0, x == y a ^ (n2 - n1)], (x.) a ^ ((e.) nInteger ? Negative) == y :> x == y a ^ (-n e), a ^ b == 1 :> b == 0 /; WeakSimplify[or[1 < a, a < -1, -1 < a < 1]], a ^ n == 0 :> and[a == 0, n > 0]}, InequalityRules] is not a valid replacement rule. : Join[OperatorRules, AbsRule, ExpressionRules, MaxMinRules, {a == b == c :> and[a == b, b == c], a ? NumberQ == b :> b == a, a b == 0 :> or[a == 0, b == 0], a + b == c :> a + (b - c) == 0 /; c =!= 0, (x.) a == (y.) a :> or[a == 0, x == y], (x.) a ^ (n1.) == (y.) a ^ (n2.) :> or[a ^ n1 == 0, x == y a ^ (n2 - n1)], (x.) a ^ ((e.) nInteger ? Negative) == y :> x == y a ^ (-n e), a ^ b == 1 :> b == 0 /; WeakSimplify[or[1 < a, a < -1, -1 < a < 1]], a ^ n == 0 :> and[a == 0, n > 0]}, InequalityRules] is not a valid replacement rule. : Union[] is not a valid replacement rule. : RulesForRelations is not a valid replacement rule. """
If I load that problematic file alone, it is just fine:
python main.py bound.mCould this be a subtle bug in Mathics?
sn6uv
commented
11 years ago It looks like a bug in Union perhaps. I also noticed that
>> (a_ != b_) :> not[a == b]on it's own raises a similar error to the first one. I'll have a look into this.
I should also point out that Mathics doesn't support the old style Mathematica syntax. For example it looks like not has been replaced with Not around Mathematica 3. Since we are aiming to support the later versions of Mathematica using not will not work under Mathics
langit
commented
11 years ago Thanks. Meanwhile, I will update the code of analytica to use 'Not' instead of 'not'.
langit
commented
11 years ago Hi, I examined the code and find out it is doing something like this in the file operator.m (it seems the author of this code is assuming the use of "Not" in Mathematica 2.2.2 -- I don't know if at version 2.2.2 of Mathematica "Not" is already used, seems there is no documentation available on the Internet):
(* Rules for "not" *)
not[True] = False;
not[False] = True;
not[not[a_]] := a;
not[and[a_, b__]] := or[not[a],not[and[b]]];
not[or[a_, b__]] := and[not[a],not[or[b]]];
not[imp[a, b]] := and[a, not[b]];
...
(* Local rules to convert Mathematica operators into our own *)
OperatorRules = {
Or -> or,
And -> and,
Not -> not
};
langit
commented
11 years ago Sorry, I noticed that the file operator.m is never loaded. It seems that "and" and "or" also need be capitalized. I will make changes and upload them to github.
langit
commented
11 years ago Hi, I have made a new branch not2Not on analytica, capitalized "and", "or" and "not". However, this does not seem to change the bugs (is_same problem and Union problem) reported above.
langit
commented
11 years ago I finally managed to run Mathematica 2.2 and verified that "Not", "And", "Or" are the actual keywords in version 2.2. The "not", "and", "or" used in analytica seems to serve the purpose of providing data structure for the proof algorithm.
langit
commented
11 years ago Interesting enough, I also noticed that
(a != b) :> Not[a == b]
on it's own also raises a similar error to the first one.
sn6uv
commented
11 years ago There was a bug in Unequal (the != operator), which has been fixed in PR #86. Let's try again with this fix.
langit
commented
11 years ago Thanks, that is indeed fixed. But I still have problems loading analytica: it simply hangs on loading the definition of GosperSum. And before that, the Join operator does complain:
Strict/: a Strict[b] := If[TrueQ[WeakSimplify[or[a>0, a<0]]], Strict[a b], a b]; : Join[OperatorRules, AbsRule, ExpressionRules, MaxMinRules, {a == b == c :> and[a == b, b == c], a ? NumberQ == b :> b == a, a b == 0 :> or[a == 0, b == 0], a + b == c :> a + (b - c) == 0 /; c =!= 0, (x.) a == (y.) a :> or[a == 0, x == y], (x.) a ^ (n1.) == (y.) a ^ (n2.) :> or[a ^ n1 == 0, x == y a ^ (n2 - n1)], (x.) a ^ ((e.) nInteger ? Negative) == y :> x == y a ^ (-n e), a ^ b == 1 :> b == 0 /; WeakSimplify[or[1 < a, a < -1, -1 < a < 1]], a ^ n == 0 :> and[a == 0, n > 0]}, InequalityRules] is not a valid replacement rule. : Join[OperatorRules, AbsRule, ExpressionRules, MaxMinRules, {a == b == c :> and[a == b, b == c], a ? NumberQ == b :> b == a, a b == 0 :> or[a == 0, b == 0], a + b == c :> a + (b - c) == 0 /; c =!= 0, (x.) a == (y.) a :> or[a == 0, x == y], (x.) a ^ (n1.) == (y.) a ^ (n2.) :> or[a ^ n1 == 0, x == y a ^ (n2 - n1)], (x.) a ^ ((e.) nInteger ? Negative) == y :> x == y a ^ (-n e), a ^ b == 1 :> b == 0 /; WeakSimplify[or[1 < a, a < -1, -1 < a < 1]], a ^ n == 0 :> and[a == 0, n > 0]}, InequalityRules] is not a valid replacement rule. : Union[] is not a valid replacement rule. : RulesForRelations is not a valid replacement rule.
Any suggestions? Thanks in advance.
sn6uv
commented
11 years ago Another issue: BeginPackage has not been properly implemented yet. There are still a few things to sort out with Mathics context (I'm working towards fixing this at #84).
langit
commented
11 years ago Thanks a lot! I'm looking forward to it. Meanwhile, the GosperSum definition actually loaded after quite some time. :) So far all complaints I have got are about
: Join[...] is not a valid replacement rule. : Union[] is not a valid replacement rule.
I am quite excited about this: it would be a nice show case to make mathics run analytica and actually prove some classical theorems (it might be slow though).
I am using my hacked main.py to load analytica. I noticed in Mathematica 8, you can simply load a file without quoting the file name. I agree with you that mathics probably should allow the same.
sn6uv
commented
11 years ago I'm still trying to figure out what's going on with the replacement rule errors.
You're right about the GrosperSum definition taking a while to load. I believe the slowness is due to the speed of the Mathics parser (a known issue). Using the PyPy interpreter instead of CPython should give a slight speed-up. On my system for example:
$> time pypy main.py index.all
...
real 3m48.566s
user 3m47.077s
sys 0m0.753
$> time python2 main.py index.all
...
real 11m38.971s
user 11m36.853s
sys 0m0.123Both of these are failing when setting $RecursionLimit. I'm not sure why this is.
poeschko
commented
11 years ago langit
commented
11 years ago I will give 2. a try -- I just started learning Mathematica, so please be patient with me. Meanwhile, this might be caused by various sources:
A. is my hack of main.py OK? I shared a single object of definitions across all loaded file, and I am not quite familiar with the internals of mathics yet. But when I look at the way mathics does it, it seems a separate definition object is used, so loading a file of definitions might not have the intended effect of loading the definitions into current scope. Again, I am new to mathics as well, so I could be wrong.
My hack includes the following features: a) allow direct loading of file (without quoting file names) with current definition object. b) allow more operators at the end of a line to expecting more input. c) allow a literal "\" at the end of a line to continue to the next line.
Meanwhile, I'm fixing some minor issues with analytica (strings running multiple lines without explicit "\"), should git-push the updates soon.
B. could it be caused by other issues here (Such as BeginPackage)? I tried to load a single file ($ python main.py lemmas.m) and there is no problem at all. I also noticed that there are a couple of other problems reported during the run. I will report them separately.
sn6uv
commented
11 years ago No update in 8 months - closing
Hi, I have skimmed through the documentation, it seems I can't read in a batch of commands saved in a file. I wonder if this is possible at all?