FriCAS-1.1.2 news
Waldek Hebisch
Please suggest additions or corrections:
FriCAS 1.1.2 news:
- Experimental Texmacs interface and Texmacs format output.
- Guessing package can now guess algebraic dependencies.
- Expansion into Taylor series and limits now work for most
special functions.
- Spad to Aldor translator is removed.
- Spad compiler no longer allows to denote sets using braces.
Bug fixes:
- Fixed few cases where elementary integrals were returned
unevalueated or produced wrong results.
- Unwanted numerical evaluation should be no longer a problem
(FriCAS interpreter now very stronly prefers symbolic
evaluation over numerical evaluation).
- Fixed a truncation bug in guessing package which causes loss
of some correct solutions.
- TeX and MathML format should correctly put parentheses around
and inside sums and products.
- Fixes few problems with handling of Unicode.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Martin Baker
Would you be interested in including an implementation of SKI
combinators?
I have put it in this file:
ski.spad.pamphlet
Which I have put here:
https://github.com/martinbaker/multivector/
Further documentation and tutorial is here:
http://www.euclideanspace.com/maths/standards/program/mycode/ski/
Martin
Waldek Hebisch
It looks like good addition for next release (possibly after some
changes) -- I would like to finish current one as soon as possible
and _then_ start adding new code.
BTW: In the message containing first version of 1.1.2 news/relase notes
when I wrote about additions I meant additions to the notes.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Martin Baker
> It looks like good addition for next release (possibly after some
> changes) -- I would like to finish current one as soon as possible
> and _then_ start adding new code.
OK, I'll wait to hear from you.
In the meantime I am working on a companion domain 'Lambda' which can be
coerced to and from the SKI combinator domain. I've also been thinking about a
third IntuitionisticLogic domain.
> BTW: In the message containing first version of 1.1.2 news/relase notes
> when I wrote about additions I meant additions to the notes.
Yes, I realised that, but I thought there may have been a small chance of
sneaking it in.
Martin
Jalaluddin Morris
I don't know whether it is in fricas or not, but I have something on my
wish list for fricas - namely the option for a / 0 = 0 for the field of
real numbers, as is standard in Isabelle/HOL, and implicit for the
pseudo-inverse in linear algebra.
Could this be engineered as a domain?
Regards,
Jalaluddin
Ralf Hemmecke
> wish list for fricas - namely the option for a / 0 = 0 for the field of
> real numbers, as is standard in Isabelle/HOL, and implicit for the
> pseudo-inverse in linear algebra.
When you speak of "field of real numbers", which domain in FriCAS do you
mean exactly? "Float" is certainly not that domain.
Do you really mean that division by zero should give zero instead of a
division-by-zero error?
Maybe related to this?
http://comments.gmane.org/gmane.comp.mathematics.maxima.general/33656
http://www.math.utexas.edu/pipermail/maxima/2011/024297.html
Ralf
Bill Page
numbers"? Are you talking about computation with exact reals? As far
as I know FriCAS does not include any implementation of exact real
arithmetic (yet). The best it can do is FLOAT, the domain of floating
point numbers with user specified precision which is only a FIELD in
an approximate sense.
> --
> You received this message because you are subscribed to the Google Groups
> "FriCAS - computer algebra system" group.
> To post to this group, send email to fricas...@googlegroups.com.
> To unsubscribe from this group, send email to
> fricas-devel...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/fricas-devel?hl=en.
>
>
Bill Page
one get if one requires x/0 = 0? It is not a field or even a division
algebra, right?
Bertfried Fauser
I have even problems with this in a sense of topological terms. `Reals' come
with a notion of approximation, so a/<very small>=<very big> and one does not
want it to be zero _suddenly_, which would make division non continuous (on
the open set reals minus 0).
The pseudo inverses I know (in linear algebra) provide partial inverses, that
is, if A is a linear operator having a null space, then you may want
to invert it on
the complement of the null space where it acts non trivially. If that
is the point,
it is surely not `a/0=0' what one does want. This looks to me much
like multiplying
by zero, which tends to transform wrong statements into true ones:
Let a<>b, a=b is false, but 0 = (a+b)/0 = a/0 + b/0 = 0 + 0 = 0 is true.
Hence such an operation destroys the equational representation of the algebraic
structure. I don't think this has to do with the difference between FLOAT and
(exact) reals... If you would represent reals exactly as streams of
digits, then
a/0 is a process which would not terminate (truth value would be `bottom' of
`undefined', neither true nor false). To do exact real number arithmetics one
does need topology.
Cheers
BF.
--
% PD Dr Bertfried Fauser
% Research Fellow, School of Computer Science, Univ. of Birmingham
% Honorary Associate, University of Tasmania
% Privat Docent: University of Konstanz, Physics Dept
<http://www.uni-konstanz.de>
% contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/
% Phone : +44-121-41-42795
Bill Page
I agree with your comments in general.
On Thu, Mar 24, 2011 at 11:50 AM, you wrote:
>
> I have even problems with this in a sense of topological terms.
> ...
>
> Hence such an operation destroys the equational representation
> of the algebraic structure. I don't think this has to do with the
> difference between FLOAT and (exact) reals...
I agree completely to this point.
> If you would represent reals exactly as streams of digits, then
> a/0 is a process which would not terminate (truth value would
> be `bottom' of `undefined', neither true nor false).
The representation of almost all exact real numbers correspond to
processes that do not terminate. In that sense I suppose a/0 is not so
different, but certain not 0.
> To do exact real number arithmetics one does need topology.
>
This is really a different subject but I would like to hear about your
views on this. Can you think of any reference that relates exact real
numbers to topology? If so, let's start another thread.
Regards,
Bill Page.
Jalaluddin Morris
It seems that my correspondence with the people at Maxima has surfaced.
I purposely avoided mentioning it I regard it as embarrassing to one of
the Maxima group, who reacted to my initial enquiry by asking
Why is this a good idea? *It is not mathematically true.*
I replied with:
Alice laughed: "There's no use trying," she said; "one can't believe
impossible things." "I daresay you haven't had much practice," said the
Queen. "When I was younger, I always did it for half an hour a day. Why,
sometimes I've believed as many as six impossible things before
breakfast." ~ Lewis Carroll from Alice in Wonderland
The truth is out there, somewhere.:)
As this particular person went on to obliquely accuse me of flaming I
gave up on Maxima, which is why I am raising the matter elsewhere, but
let me quote from a draft of a book I am writing:
--------------------
The perspicacious reader may notice that in two subsections of this
chapter life is made easier by
the assumption that for the field of real numbers a/0 = 0 , despite the
comment from one person
that �It is not mathematically true.� Note that by so doing we are in
the company of Isabelle/HOL.
The author�s advice to anyone who might question this assumption is to
1. within the context of the field axioms prove that a/0 is undecidable,
reflect on the consequences
of G�del�s Theorem, and then relax, or
2. prove that a/0 is false, then contact the author of this book and the
Isabelle group, preferably
providing dunces hats for us to wear.
--------------------
This quote gives my position and I can really only ask that you reflect,
more carefully than I believe has the person quoted above, when
considering division by zero.
Regards,
Jalaluddin
Waldek Hebisch
> Martin,
>
> I don't know whether it is in fricas or not, but I have something on my
> wish list for fricas - namely the option for a / 0 = 0 for the field of
> real numbers, as is standard in Isabelle/HOL, and implicit for the
> pseudo-inverse in linear algebra.
>
> Could this be engineered as a domain?
>
Compile the following:
-------------------<cut here>------------------------
)abbrev category NFIELDC NewFieldCategory
NewFieldCategory : Category == Field with
ndiv : (%, %) -> %
add
x, y : %
x / y == ndiv(x, y)
)abbrev domain NFIELD NewField
NewField(F : Field) : NewFieldCategory
== F add
ndiv(x : %, y : %) : % ==
y pretend F =$F 0$F => 0$F pretend %
(x pretend F /$F y pretend F) pretend %
------------------<cut here>--------------------------
Then you can do:
(1) -> nF := NewField(Fraction(Integer))
(1) NewField(Fraction(Integer))
Type: Type
(2) -> 1$nF / 0$nF
(2) 0
Type: NewField(Fraction(Integer))
In other words, given a normal FriCAS field you can get new field
like the old one, but with new division.
You probably also want to redefine 'divide' and possiby other
functions.
BTW: I tried simpler definition, without extra category and 'ndiv'
function, but for some reason Spad compiler did not like it.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Waldek Hebisch
>
> Thanks Ralf, that makes a bit more sense. What exactly (formally) does
> one get if one requires x/0 = 0? It is not a field or even a division
> algebra, right?
>
Well, x/0 = 0 is pretty standard in logic: in logic one wants
total functions so _some_ definition of x/0 is required. Then
using 0 as a value is most natural. If you want to stay in
the "most classical logic", that is first order logic with
total functions, then FriCAS field is not a legitimate mathematical
structure, becase in FriCAS division is a partial function
(so for FriCAS you need "stronger" logic).
The intent of this definition is that you really do not want to
compute things like 1/0, but for formal reasons you can not avoid
them. Consider:
(x ~= 0) and (z = 1/x)
This is a fine, sensible logical formula: when 'x' is 0 then the
formula is false due to first term and if 'x' is different from 0,
then division is well-defined. But if 'and' is a function and
we evaluate arguments first we may be forced to compute '1/0',
use it in comparison and then effectively throw out the result
of the comparison.
Of course, if one really makes use of exact value of x/0 then
it is confusing...
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Bill Page
for x/0. This is not so different than considering the CardinalNumber
domain as an extension of NonNegativeInteger. CardinalNumber is not
used much in FriCAS except as the domain of the operation 'dimension'
(of VectorSpace, etc.) however it includes a value of Aleph(0) for
infinite cardinality. I suppose that it would be possible to define
something like this for Float, e.g.
x/0 = Aleph(1)
and we have
x ~= Aleph(1)
for all values in Float except Aleph(1).
But I worry if the proposal really is that
x/0 = 0
since that could do a lot of damage to many other desirable properties that
Float has Field
should imply, e.g. as Bertfried pointed out concerning it's
topological properties.
I agree that FriCAS (and mathematics in general) needs a stronger more
general logic. In fact isn't "higher order logic" the main point of
Isabelle/HOL? Therefore I do not understand why Jalaluddin Morris
claims that Isabelle/HOL somehow legitimizes this choice for the
"field of real numbers".
Regards,
Bill Page.
Gabriel Dos Reis
| This is not so different than considering the CardinalNumber
| domain as an extension of NonNegativeInteger. CardinalNumber is not
| used much in FriCAS except as the domain of the operation 'dimension'
| (of VectorSpace, etc.) however it includes a value of Aleph(0) for
| infinite cardinality.
I have always considered it a weakness that VectorSpace did not use
CardinalNumber for dimension -- even if for all practical purposes
NonNegativeInteger is sufficient and more efficient. That, in my
opinion, calls for an efficient abstraction, e.g. find a way to
support CardinalNumber and make the common cases as efficient as
NonNegativeInteger.
(please don't mention `subsumption', I don't want to go there.)
-- Gaby
Bill Page
Is this a typo? Or a recent change?
As far as I can see VectorSpace *does* export dimension with a result
in CardinalNumber. I suppose that in most usages is it simply
converted to NNI.
Regards,
Bill Page.
Bertfried Fauser
I attended today a talk by Martin Escardo, Birmingham, who is a
specialist on exact real
number computations. The attached literate haskel program explains a
bit what he is doing,
it is available from his website http://www.cs.bham.ac.uk/~mhe/ (see
publications and search
for `fun' somewhat down, there is also a paper)
The main point I wanted to make, is that to be able to define
computable functions, one needs
to have continuity, that is topology. To device a programming
language, Escardo has developed
a fully abstract programming language. But one can easily check that
for example only constant
functions Reals ---> Bool are computable, so for example a test of
equality is not available
for (exact) Reals. In my eyes (and Escardo seems to support this) a
setting as a/0=0 cannot
be continuous, it drops hence out of that theory. Anyhow, how to
detect if b is zero, so that a/b=0?
That is all I can contribute, I am not an expert in these things, so a
new thread is not needed.
Cheers
BF.
Waldek Hebisch
>
> Thanks Waldek. I don't really have a problem with providing a value
> for x/0. This is not so different than considering the CardinalNumber
> domain as an extension of NonNegativeInteger. CardinalNumber is not
> used much in FriCAS except as the domain of the operation 'dimension'
> (of VectorSpace, etc.) however it includes a value of Aleph(0) for
> infinite cardinality. I suppose that it would be possible to define
> something like this for Float, e.g.
>
> x/0 = Aleph(1)
>
> and we have
>
> x ~= Aleph(1)
>
> for all values in Float except Aleph(1).
>
Bill, I am afraid you did not notice the main point: in classical
logic we want total functions. If you add sometning like Aleph(1)
you need to define all field operations on Aleph(1). If you add
a single element then there is _no way_ to extend operations
so that field axioms are satified. If you add more elements
than what you are doing is effectively replacing your original
field by a bigger one and than choosing value for '1/0' _in this
bigger field_. In other words, to make '/' into a total function
you have to choose value for '1/0' _inside_ the field.
> But I worry if the proposal really is that
>
> x/0 = 0
>
> since that could do a lot of damage to many other desirable properties that
>
> Float has Field
>
> should imply, e.g. as Bertfried pointed out concerning it's
> topological properties.
Float is bad example because strictly speaking it is not a field
(operations are nonassociative). However defining 'x/0' does not
really change properties of field: normal field axioms only say
what happens when you divide by nonzero element.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Bill Page
On Fri, Mar 25, 2011 at 1:01 PM, you wrote:
> Bill Page wrote:
>>
>> Thanks Waldek. I don't really have a problem with providing a value
>> for x/0. This is not so different than considering the CardinalNumber
>> domain as an extension of NonNegativeInteger. CardinalNumber is not
>> used much in FriCAS except as the domain of the operation 'dimension'
>> (of VectorSpace, etc.) however it includes a value of Aleph(0) for
>> infinite cardinality. I suppose that it would be possible to define
>> something like this for Float, e.g.
>>
>> x/0 = Aleph(1)
>>
>> and we have
>>
>> x ~= Aleph(1)
>>
>> for all values in Float except Aleph(1).
>>
>
> Bill, I am afraid you did not notice the main point: in classical
> logic we want total functions. If you add sometning like Aleph(1)
> you need to define all field operations on Aleph(1). If you add
> a single element then there is _no way_ to extend operations
> so that field axioms are satified. If you add more elements
> than what you are doing is effectively replacing your original
> field by a bigger one and than choosing value for '1/0' _in this
> bigger field_. In other words, to make '/' into a total function
> you have to choose value for '1/0' _inside_ the field.
>
I think I do understand the main point.
I do not think it is possible to do this _inside_ the field of real
numbers. Any way you do this the result cannot be a Field (or even a
Ring), however it might still be useful
http://en.wikipedia.org/wiki/Real_projective_line
where Aleph(1) = - Aleph(1)
Or
http://en.wikipedia.org/wiki/Extended_real_number_line
where there are both + and - infinities.
>> But I worry if the proposal really is that
>>
>> x/0 = 0
>>
>> since that could do a lot of damage to many other desirable properties that
>>
>> Float has Field
>>
>> should imply, e.g. as Bertfried pointed out concerning it's
>> topological properties.
>
> Float is bad example because strictly speaking it is not a field
> (operations are nonassociative).
True. I assumed that we were already glossing over that issue.
> However defining 'x/0' does not
> really change properties of field: normal field axioms only
> say what happens when you divide by nonzero element.
If the inverse of 0 is 0 then the domain should not even be a Group
let alone a Field.
But I think your example of how to define such a domain in FriCAS is
still interesting. I am curious why it seemed to be more difficult to
do this than one might have expected. Are there some hidden
assumptions somewhere in FriCAS about Float?
Regards,
Bill Page.
Waldek Hebisch
> >> But I worry if the proposal really is that
> >>
> >> x/0 = 0
> >>
> >> since that could do a lot of damage to many other desirable properties
> that
> >>
> >> Float has Field
> >>
> >> should imply, e.g. as Bertfried pointed out concerning it's
> >> topological properties.
> >
> > Float is bad example because strictly speaking it is not a field
> > (operations are nonassociative).
>
> True. I assumed that we were already glossing over that issue.
>
> > However defining 'x/0' does not
> > really change properties of field: normal field axioms only
> > say what happens when you divide by nonzero element.
>
> If the inverse of 0 is 0 then the domain should not even be a Group
> let alone a Field.
>
Let us recall field axioms:
1) field is abelian group with respect to addition. Defining 1/0 = 0
does not affect this at all.
2) _nonzero_ elements of the field form an abelian group with
respect to multiplication. Again defining 1/0 = 0, because
here we consider only nonzero elements (using 1/0 = x with
nonzero x would be more tricky)
3) distributive law:
\forall_{a, b, c} a*(b+c) = a*b + a*c
Since distributive law does not involve division it is satisfied
if 1/0 = 0.
The axioms imply \forall_a 0*a = 0. This is fundamental property
of fields and means that it is impossible to define 1/0 in such a
way that _all_ elements of field form multiplicative group.
> But I think your example of how to define such a domain in FriCAS is
> still interesting. I am curious why it seemed to be more difficult to
> do this than one might have expected. Are there some hidden
> assumptions somewhere in FriCAS about Float?
Nothing special about Float. Spad compiler signals type error
in simpler code -- ATM I do not know if there is some problem
with simpler code or it is a compiler bug.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Bill Page
Thanks for your patient explanation. So we define
1/0 = 0
but we do not call this a multiplicative inverse. Should we say then that
0^(-1)
is still undefined?
Regards,
Bill Page.
Waldek Hebisch
>
> Waldek,
>
> Thanks for your patient explanation. So we define
>
> 1/0 = 0
>
> but we do not call this a multiplicative inverse. Should we say then that
>
> 0^(-1)
>
> is still undefined?
>
What is defined depends on exact definitions in use. If field
axioms use inverse denoted by x^(-1), then of course 0^(-1)
is defined. If field axioms use '/' then 'x^(-1)' is probably
undefined and then also '0^(-1)' is undefined. In the constructor
I posted only '1/0' is defined, for '0^(-1)' one would have to add
extra code.
One more remark: we are talking about "formal systems" here.
There are no deep meaning here, like in case of empty set formal
definitions may be sligthly different than intuition, but are
made so that formal systems works well for specific purpose
(in our case for "first order" theory of fields). If you
look for meaning and want to allow '1/0' you will probably use
different mathematical structure (like projective plane), which
however is no longer a field.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Jalaluddin Morris
I suggest "park" as it is a bit bigger than a field, or "padang" which
is Malay for field, but perhaps a name could be agreed on with the
participation of the Isabelle/HOL people.
Jalaluddin
Bill Page
On Mon, Mar 28, 2011 at 12:54 PM, you wrote:
> Bill Page wrote:
>> Thanks for your patient explanation. So we define
>>
>> 1/0 = 0
>>
>> but we do not call this a multiplicative inverse. Should we say then that
>>
>> 0^(-1)
>>
>> is still undefined?
>>
>
> What is defined depends on exact definitions in use. If field
> axioms use inverse denoted by x^(-1), then of course 0^(-1)
> is defined.
But presumably by definition x^(-1) denotes the multiplicative inverse
x * x^(-1) = 1
and 0^(-1) is not such an inverse. It is interesting, maybe that
FriCAS gives different error messages for these two cases:
1.0/0.0
and
(0.0)^(-1)
> If field axioms use '/' then 'x^(-1)' is probably
> undefined and then also '0^(-1)' is undefined. In the constructor
> I posted only '1/0' is defined, for '0^(-1)' one would have to add
> extra code.
>
What value would you give it?
> One more remark: we are talking about "formal systems" here.
> There are no deep meaning here, like in case of empty set formal
> definitions may be sligthly different than intuition, but are
> made so that formal systems works well for specific purpose
> (in our case for "first order" theory of fields). If you
> look for meaning and want to allow '1/0' you will probably use
> different mathematical structure (like projective plane), which
> however is no longer a field.
>
Since FriCAS is a computer *algebra* system and not a automated proof
system it is not clear to me in what sense FricCAS currently supports
a first order theory of fields but of course one can program FriCAS in
a general manner for many different purposes.
As I suggested earlier my preference would definitely be to consider a
domain representing the projective plane (unsigned infinity) or maybe
a two point compactification (signed infinity) rather than one in
which we have a/0=0.
Regards,
Bill Page.
Gabriel Dos Reis
[ replying late. ]
Bill Page <bill...@newsynthesis.org> writes:
| Gaby,
|
| Is this a typo? Or a recent change?
A typo -- sorry.
Gabriel Dos Reis
[...]
| > However defining 'x/0' does not
| > really change properties of field: normal field axioms only
| > say what happens when you divide by nonzero element.
|
| If the inverse of 0 is 0 then the domain should not even be a Group
| let alone a Field.
I am not sure that is the real issue.
The real problem is if you take that axiom, what parts of the usual
classical theorems remain true and to what extent?
Anybody wants to make the function
x +-> exp(-1/x^2)
discontinue at x=0? How much of Real Analysis do you have to redefine?
The notion that "it is done in Isabelle/HOL therefore it must be right"
has to be tempered with the fact that Isabelle/HOL is a
*logical framework* in which one develops logics. What is often left
under-appreciated is that there are -many- logics used to prove this and
that theorem, but we don't have yet a coherent set of logics to
handle all that has been accomplished in computational mathematics.
Of course, if you are into Calculemus, you already know this.
-- Gaby
Juan Jose Garcia-Ripoll
- It was not obvious to me that Fricas had a graphical interface. This prevented me from using for some time. Some notes about how to start fricas and how to best use it would be welcome for newbies.
- I use OS X. This is another reason why I was not able to use the graphical interface: one has to explictly supply --x-includes and --x-libraries. Would it be possible to automatically detect this?
- I had to fix ECL on a couple of places. The problem is that is a file on Fricas called float.lsp. This float.lsp, when compiled, leads to a float.h which,as you may guess, conflicts with /usr/include/float.h I have changed the extension of header files in CVS, so that now the files generated will be float.c float.eclh and float.data, no conflicts expected.
- Fricas from CVS fails to build at all with ECL. Unfortunately SBCL from Fink also does not build Fricas. I believe the problems are totally unrelated, but I would like to be able to debug the problem with Fricas: all I get is an "Internal Error" message, no debugger, no hints on how to proceed.
Waldek Hebisch
>
> Hi Waldek, congratulations for Fricas. I started using it recently and I am
> very impressed. I have some comments.
>
Thanks for kind words.
>
> - It was not obvious to me that Fricas had a graphical interface. This
> prevented me from using for some time. Some notes about how to start fricas
> and how to best use it would be welcome for newbies.
> - I use OS X. This is another reason why I was not able to use the
> graphical interface: one has to explictly supply --x-includes and
> --x-libraries. Would it be possible to automatically detect this?
I do not know: FriCAS uses autoconf. So it should work or fail in
similar way as other autoconf-using programs. FriCAS do performs
a few extra checks, notably for Xpm library so they are likely culprit.
Could you send me output of 'configure' (in particular 'config.log')?
> - I had to fix ECL on a couple of places. The problem is that is a file
> on Fricas called float.lsp. This float.lsp, when compiled, leads to a
> float.h which,as you may guess, conflicts with /usr/include/float.h
> I have
> changed the extension of header files in CVS, so that now the files
> generated will be float.c float.eclh and float.data, no conflicts expected.
> - Fricas from CVS fails to build at all with ECL. Unfortunately SBCL from
> Fink also does not build Fricas. I believe the problems are totally
> unrelated, but I would like to be able to debug the problem with Fricas: all
> I get is an "Internal Error" message, no debugger, no hints on how to
> proceed.
>
Apparently you are building on case-insentive filesystem (otherwise
there should be no conflict between "FLOAT.h" and "float.h").
That in the past we tried to eliminate conflicts due to filenames
clashing when compared in case-insentive way, but I am not sure
if this was recently tried. Anyway, looks like possible common
problem.
If you have build FriCAS (or build advanced far enough) then
)set break break
at FriCAS command line make FriCAS error handler execute "BREAK"
on error, so you get dropped into Lisp debugger. When debugging
build problems I run 'make' with output redirected to a file,
like
make > mlogg
when build fails I look trough log to find first error (ATM build
may contunue much beyond the core failure point). Then
I interactively re-run failing command. At early stages
executables like 'lisp', 'bootsys' and 'depsys' just present
normal Lisp prompt. Later 'interpsys' and 'AXIOMsys' use
FriCAS prompt.
When using ECL you may want to change ecl-specific part at the
end of src/lisp/fricas-package.lisp (currently this part
sets safety to 1, but for debugging one should probably use
higher debug setting).
> I believe it should be pretty easy to bundle Fricas and ECL in a DMG bundle
> for easy distribution in OS X. You may consider this for the upcoming
> release.
>
I have no access to OS X. However, if somebody provided such combination
I would be happy to put it on sourceforge for download.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Xiaojun Liu
--
Best regards,
On 2011年4月12日星期二 at 上午2:48, Waldek Hebisch wrote:
Juan Jose Garcia-Ripoll wrote:
Hi Waldek, congratulations for Fricas. I started using it recently and I am
very impressed. I have some comments.
Thanks for kind words.
- It was not obvious to me that Fricas had a graphical interface. This
prevented me from using for some time. Some notes about how to start fricas
and how to best use it would be welcome for newbies.
- I use OS X. This is another reason why I was not able to use the
graphical interface: one has to explictly supply --x-includes and
--x-libraries. Would it be possible to automatically detect this?
I do not know: FriCAS uses autoconf. So it should work or fail in
similar way as other autoconf-using programs. FriCAS do performs
a few extra checks, notably for Xpm library so they are likely culprit.
Could you send me output of 'configure' (in particular 'config.log')?
- I had to fix ECL on a couple of places. The problem is that is a file
on Fricas called float.lsp. This float.lsp, when compiled, leads to a
float.h which,as you may guess, conflicts with /usr/include/float.h
I have
changed the extension of header files in CVS, so that now the files
generated will be float.c float.eclh and float.data, no conflicts expected.
- Fricas from CVS fails to build at all with ECL. Unfortunately SBCL from
Fink also does not build Fricas. I believe the problems are totally
unrelated, but I would like to be able to debug the problem with Fricas: all
I get is an "Internal Error" message, no debugger, no hints on how to
proceed.
I have no access to OS X. However, if somebody provided such combination
I would be happy to put it on sourceforge for download.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
--
Bill Page
case: 'subtractIfCan' in NonNegativeInteger. If might be surprising
how often this is used in the Axiom code. In OpenAxiom Gaby has raised
this sort of construction
Union("failed",X)
to the level of special support for the domain constructor
Maybe(X)
in the Spad language. I think this is a good thing! :) In a sense this
allows the function
f : A -> Maybe(B)
to be "partial" but it goes much deeper than that.
It occurs to me to ask the more "algebraic" question of: "What if we
did the same thing to subtraction in NonNegativeIntegers as was
proposed here for division?" I.e. Just make it equal to 0. How much
algebra would that break? Currently we have
(1) -> (1-2)$NNI
The function - is not implemented in NonNegativeInteger .
but that is rather inconvenient sometimes and results in non-compact
coding styles such as
(r:=substractIfCan(x,y)) case "failed" => z:=0; z:=r
or worse! Of course the point is that often you migth want to do
something else as a result of the boundary condition other than just
setting the result to zero.
In the interpreter we can write:
(1) -> subtractIfCan(2,1)$NNI + 1
(1) 2
Type: PositiveInteger
But there is some magic going on here. If we try to do this in the
compiler things are more difficult. One might argue: just as they
should be! :)
One potentially really good thing about the Maybe domain constructor
in OpenAxiom is to try to have it both ways: for the most part we can
operate on the domain Maybe(X) in almost the same way as the original
domain X, i.e. have the special support for 'Maybe' try to make this
(mostly) invisible.
Anyway, what do you think of the proposal to implement '-' in
NonNegativeInteger such that
(1-2)$NNI
would return 0? Does this mean then that NonNegativeInteger could be
considered an AbelianGroup?
Bill Page.
Juan Jose Garcia-Ripoll
Juan Jose Garcia-Ripoll wrote:> - I use OS X. This is another reason why I was not able to use the
> graphical interface: one has to explictly supply --x-includes and
> --x-libraries. Would it be possible to automatically detect this?I do not know: FriCAS uses autoconf. So it should work or fail in
similar way as other autoconf-using programs.
Could you send me output of 'configure' (in particular 'config.log')?
Apparently you are building on case-insentive filesystem (otherwise
there should be no conflict between "FLOAT.h" and "float.h").
If you have build FriCAS (or build advanced far enough) then
)set break break
at FriCAS command line make FriCAS error handler execute "BREAK"
> I believe it should be pretty easy to bundle Fricas and ECL in a DMG bundle
> for easy distribution in OS X. You may consider this for the upcoming
> release.
>I have no access to OS X. However, if somebody provided such combination
I would be happy to put it on sourceforge for download.
Ralf Hemmecke
> NonNegativeInteger such that
>
> (1-2)$NNI
>
> would return 0? Does this mean then that NonNegativeInteger could be
> considered an AbelianGroup?
For which purpose do you need such a subtraction?
Programmers are lazy, and I guess, such a definition might lead to bugs
that are hard to detect.
Why do you think that turns NNI into a AbelianGroup? What's the inverse
of 2?
Ralf
Bill Page
Waldek Hebisch
> All this discussion of divide by zero made me think of another similar
> case: 'subtractIfCan' in NonNegativeInteger. If might be surprising
> how often this is used in the Axiom code. In OpenAxiom Gaby has raised
> this sort of construction
>
> Union("failed",X)
>
> to the level of special support for the domain constructor
>
> Maybe(X)
>
> in the Spad language. I think this is a good thing! :) In a sense this
> allows the function
>
> f : A -> Maybe(B)
>
> to be "partial" but it goes much deeper than that.
>
> It occurs to me to ask the more "algebraic" question of: "What if we
> did the same thing to subtraction in NonNegativeIntegers as was
> proposed here for division?" I.e. Just make it equal to 0. How much
> algebra would that break?
Just to make thing clear: I do not see _logical_ problem with
defining 1/0 to be 0. I did not propose changes to existing domains,
and in fact I think that such change would be undesirable.
Namely, current behaviour catches errors reasonably early.
After change unitended division by 0 would be hard to detect.
If someone needs 1/0 to be 0, then _new_ user defined domain
can do this (and I posted code implementing this behaviour).
I consider the fact that such constructor is relatively easy
to write and should work reasonably well together with
rest of algebra as strength of original Axiom design.
OTOH I do not encourage usage of such code: there are
strong pragmatic reasons which make 1/0 being error
preferable to getting 0. However, pragmatic reasons
are related to user needs and specific needs may
change preffered result of 1/0.
> Currently we have
>
> (1) -> (1-2)$NNI
>
> The function - is not implemented in NonNegativeInteger .
>
> but that is rather inconvenient sometimes and results in non-compact
> coding styles such as
>
> (r:=substractIfCan(x,y)) case "failed" => z:=0; z:=r
>
> or worse! Of course the point is that often you migth want to do
> something else as a result of the boundary condition other than just
> setting the result to zero.
>
> In the interpreter we can write:
>
> (1) -> subtractIfCan(2,1)$NNI + 1
>
> (1) 2
> Type: PositiveInteger
>
> But there is some magic going on here.
The only magic is automatic coercion from union to integer:
(1) -> subtractIfCan(2,1)$NNI
(1) 1
Type: Union(NonNegativeInteger,...)
(2) -> subtractIfCan(1,2)$NNI
(2) "failed"
Type: Union("failed",...)
> If we try to do this in the
> compiler things are more difficult. One might argue: just as they
> should be! :)
>
> One potentially really good thing about the Maybe domain constructor
> in OpenAxiom is to try to have it both ways: for the most part we can
> operate on the domain Maybe(X) in almost the same way as the original
> domain X, i.e. have the special support for 'Maybe' try to make this
> (mostly) invisible.
>
> Anyway, what do you think of the proposal to implement '-' in
> NonNegativeInteger such that
>
> (1-2)$NNI
>
> would return 0? Does this mean then that NonNegativeInteger could be
> considered an AbelianGroup?
>
This variant is known as "saturating" operation. Since it is not
the inverse of addition you do not get a group. I think that
pragmatic reasons (error checking) go strongly against having
such '-' in NonNegativeInteger. Note that:
(3) -> 1$NNI - 2$NNI
(3) - 1
Type: Integer
works, that is you can use '-' for NonNegativeInteger, but
the result is of type Integer. If there is enough
need we could add saturationg subtraction to to NonNegativeInteger,
but under different name (but I think that it is used rarely and
when needed we can use equivalent code using 'max' and '::')
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Waldek Hebisch
> | > really change properties of field: normal field axioms only
> | > say what happens when you divide by nonzero element.
> | If the inverse of 0 is 0 then the domain should not even be a Group
> | let alone a Field.
>
> I am not sure that is the real issue.
>
> The real problem is if you take that axiom, what parts of the usual
> classical theorems remain true and to what extent?
> Anybody wants to make the function
>
> x +-> exp(-1/x^2)
>
A little nitpick: precise traditional definition of such function
is 'exp(-1/x^2) for x ~= 0, 0 for x = 0'. This definition does
not depend on what happens with '1/x' at x = 0.
> How much of Real Analysis do you have to redefine?
If you mean Analysis in informal sense then basicaly nothing. If
you mean some set of theorems encoded in mechanically checkable
formal language, then the problem is essentially of translation
between closely related formal languages: practice has shown
that seemingly trival differences may cause trouble. OTOH
apparently at least one such set of theorems (that of Isablelle/HOL)
already uses this convention, so you will have to "patch"
existing theorems when you want different convention.
> The notion that "it is done in Isabelle/HOL therefore it must be right"
> has to be tempered with the fact that Isabelle/HOL is a=20
> *logical framework* in which one develops logics. What is often left
> under-appreciated is that there are -many- logics used to prove this and
> that theorem, but we don't have yet a coherent set of logics to
> handle all that has been accomplished in computational mathematics.
> Of course, if you are into Calculemus, you already know this.
>
As I wrote in another message: there is no _logical_ problem
with 1/0 being 0. Pragmatics of theorem prover make it
quite reasonable (but prover based on partial functions and
leaving 1/0 udefined looks quite reasonable too). Pragmatics
of CAS differs very much form pragmatics of theorem prover
and for CAS getting error on 1/0 is much better. But if
somebody wants to swap computations between CAS and
theorem prover using '1/0 = 0' convention, than having
this convention also in CAS starts looking reasonable
(reasonable enough to implement special domain with such
behaviour).
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Gabriel Dos Reis
| Gabriel Dos Reis wrote:
| >
| > Bill Page <bill...@newsynthesis.org> writes:
| >
| > [...]
| >
| > | >=A0However defining 'x/0' does not
| > | > really change properties of field: normal field axioms only
| > | > say what happens when you divide by nonzero element.
| > |=20
| > | If the inverse of 0 is 0 then the domain should not even be a Group
| > | let alone a Field.
| >
| > I am not sure that is the real issue.
| >
| > The real problem is if you take that axiom, what parts of the usual
| > classical theorems remain true and to what extent?
| > Anybody wants to make the function
| >
| > x +-> exp(-1/x^2)
| >
| > discontinue at x=?
|
| A little nitpick: precise traditional definition of such function
| is 'exp(-1/x^2) for x ~= 0, 0 for x = 0'. This definition does
| not depend on what happens with '1/x' at x = 0.
The operational keyword is *discontinue*.
If you make 1/0 = 0 then, by definition, the function
x +-> exp(-1/x^2)
is defined everywhere, including at 0 where it takes the value 1, not 0.
And that definition is just as precise as it can get.
| > How much of Real Analysis do you have to redefine?
|
| If you mean Analysis in informal sense then basicaly nothing. If
I mean the body of knowledge accumulated under the heading of
Real Analysis.
| you mean some set of theorems encoded in mechanically checkable
| formal language, then the problem is essentially of translation
| between closely related formal languages: practice has shown
| that seemingly trival differences may cause trouble. OTOH
I'm not just looking at the practice -- because I don't want to equate
"unfamiliar" with "wrong". As a scholar, I want to look at the
logical consequences.
| apparently at least one such set of theorems (that of Isablelle/HOL)
| already uses this convention, so you will have to "patch"
| existing theorems when you want different convention.
|
| > The notion that "it is done in Isabelle/HOL therefore it must be right"
| > has to be tempered with the fact that Isabelle/HOL is a=20
| > *logical framework* in which one develops logics. What is often left
| > under-appreciated is that there are -many- logics used to prove this and
| > that theorem, but we don't have yet a coherent set of logics to
| > handle all that has been accomplished in computational mathematics.
| > Of course, if you are into Calculemus, you already know this.
| >
|
| As I wrote in another message: there is no _logical_ problem
| with 1/0 being 0.
I don't think I ever suggested there is a fundamental logical problem
with 1/0 - 0. However, what I do suggest is that I've not yet seen a
single logical framework that contains all the "conventions" (that make
some proofs go through nicely, even if they are not conventional)
in a single place that handles Real Analysis. I've seen bits and pieces.
Waldek Hebisch
>
> On Monday, April 11, 2011 8:48:58 PM UTC+2, Waldek Hebisch wrote:
> >
> > Juan Jose Garcia-Ripoll wrote:
> >
> > > - I use OS X. This is another reason why I was not able to use the
> > > graphical interface: one has to explictly supply --x-includes and
> > > --x-libraries. Would it be possible to automatically detect this?
> >
> > I do not know: FriCAS uses autoconf. So it should work or fail in
> > similar way as other autoconf-using programs.
> >
> I guess the problem is that the standard include path does not include
> /usr/X11/include. It is odd, but it is so in OS X. Maybe a hint in the
> README would suffice.
>
> > Could you send me output of 'configure' (in particular 'config.log')?
> >
> As I said
> ...
> configure:7585: gcc -o conftest -g -O2 conftest.c -lX11 >&5
> ld: library not found for -lX11
> collect2: ld returned 1 exit status
That is error from the linker, so presumably something like
'-L/usr/X11/lib' is missing. If OS X has established convention
where to find X libraries we could try to add appropriate '-L...'
option to linker flags. But on most systems this on not that
easy: locations change in newer versions, there is difference
between 32 and 64 bits, etc. Googling suggests that at least
some OS X versions simply keep X libraries in /usr/lib (in such
case the test above should pass).
> Apparently you are building on case-insentive filesystem (otherwise
> > there should be no conflict between "FLOAT.h" and "float.h").
> >
> Indeed, and this was the only source of problems. The rest seems just fine.
>
>
> > If you have build FriCAS (or build advanced far enough) then
> >
> > )set break break
> >
> > at FriCAS command line make FriCAS error handler execute "BREAK"
> >
> The problem is that FriCAS does not finish building and the SBCL image does
> not even boot properly. BTW, answering Xiaojun's question, I am using a more
> recent version of SBCL, 1.0.45, shipped with Fink for 64bits.
>
> I would like to know what happens with the ECL build and why it does not
> work. Is it possible to set up a similar handler somewhere in the boot
> scripts forcing FriCAS to enter the lisp debugger or something like that?
>
I am affraid we are miscomunicating. FriCAS build system works
like build system of C program with main difference beeging that
instead of calling C compiler FriCAS uses commands like:
echo '(progn (boottran::boottocl "$<" "$@") (${BYE}))' | ${DEPSYS}
In other words appropriate Lisp images reads a command from the pipe.
Since commands are read via pipe it is inconvenient (or maybe even
impossible) to start Lisp debugger from build system. OTOH build
commands only change filesystem and have no persistent effect on
Lisp executing them, so to debug it in enough to execute "by hand"
the failing command. There are several images used during build,
of them 2 give you FriCAS prompt, the other normal Lisp prompt.
If you execute Lisp image like 'depsys' normal Lisp error
handling is in place, so Lisp level errors bring you into debugger
(however for this you need to run command by hand, if commands are
read from pipe then Lisp image just exits).
The main work in first stages of build is done by 'bootsys' and
'depsys'. 'bootsys' and 'depsys' translate Boot code into Lisp.
If any of them discovers error during translation it prints
error message and comes back to the Lisp prompt. As I wrote
Lisp level error in 'bootsys' or 'depsys' get normal Lisp
handling.
I plan to modify 'bootsys' and 'depsys' to exit on errors
with nonzero exit code. Of course, doing that I can add option
to activate Lisp debugger. However, in my experience most
errors during build were Lisp level error so this will change
situation only a little.
Currently debugging build problems is harder than it should be
because Lisp image continues to run after error and eventually
exits with 0 exit code, so 'make' thinks that everything is
OK and runs subseqent commands. Consequently it requires some
effort to find first failing command (the first one usually
is real culprit, the other just a consequence). Exiting with
nonzero code should solve this problem.
BTW: If you send me (via private mail) output of
make > mlogg
I should be able to tell you which command is responsible for
failure and how to debug this failure.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Eugene Surowitz
I seem to remember that it might be a part of the "Xcode"(? exact name) package.
Eugene J. Surowitz
Juan Jose Garcia-Ripoll
Do you have Apple's X development system even installed?
I seem to remember that it might be a part of the "Xcode"(? exact name) package.
--
Instituto de Física Fundamental, CSIC
c/ Serrano, 113b, Madrid 28006 (Spain)
http://juanjose.garciaripoll.googlepages.com
Waldek Hebisch
1) I believe that '1/0 = 0' can be used as part of faithful
formalization of Real Analysis. In fact, if you are
interested in elementary part (meaning no sets, no sequences, ...)
and use logic with total functions than there seem to be
no good alternative.
2) As practicioner of Real Analysis I am not interested in conseqences
of '1/0 = 0' -- as I wrote I believe that they do not affect
important matters (in particular system remains consistent).
Of course you may have different opinion.
Coming back to 'exp(-1/x^2)': with '1/0 = 0' this function
formally is discontinuous. Informal reaction is that
you either have wrong definition or ask wrong question
(note that informally uniteresting question is a kind of
wrong question). The point is that sometimes you do not
care what happens at zero and then '1/0 = 0' "works",
sometimes you care, then one has to do definition via
cases.
> | apparently at least one such set of theorems (that of Isablelle/HOL)
> | already uses this convention, so you will have to "patch"
> | existing theorems when you want different convention.
> |
> | > The notion that "it is done in Isabelle/HOL therefore it must be right"
> | > has to be tempered with the fact that Isabelle/HOL is a=20
> | > *logical framework* in which one develops logics. What is often left
> | > under-appreciated is that there are -many- logics used to prove this and
> | > that theorem, but we don't have yet a coherent set of logics to
> | > handle all that has been accomplished in computational mathematics.
> | > Of course, if you are into Calculemus, you already know this.
> | >
> |
> | As I wrote in another message: there is no _logical_ problem
> | with 1/0 being 0.
>
> I don't think I ever suggested there is a fundamental logical problem
> with 1/0 - 0. However, what I do suggest is that I've not yet seen a
> single logical framework that contains all the "conventions" (that make
> some proofs go through nicely, even if they are not conventional)
> in a single place that handles Real Analysis. I've seen bits and pieces.
I do not think you will find a single logical framework that directly
contains all popular conventins. IMHO various conventions are more
like macros in programing languages: they are created to fit
single problem (or domain) and are too specialised to work in
general. Logical framework may (and probably should) contain
a preprocessor to expand statements into canonical form. One
can imagine predefined "macro files" with conventions for
various domains.
Let me add that IMHO when talking about logical framework for
some part of mathematics like Real Analysis one needs mechanical
checking (people are resonably good at inventing and writing
down proofs, but formal checking is too tedious for them).
And doing Real Analysis really means doing all mathematics.
AFAICS current checking systems are limited. One problem
is that to give short proof one needs large volume of
preexisting knowledge (theorems). Connected problem is
that proofs encoded in procedural systems are hard to
read for even for specialists. Some people seem to believe
that if we keep encoding existing theorems in existing
systems then eventually system will have enough "base
knowledge" to allow writing real research results.
I somewhat doubt this: IMHO proof checking systems
should process mathematics in smarter ways. It seems
that when dealing with logic current systems are
more capable than humans. But humans works at many levels:
pragmatics (what is doable and what is intersting),
procedural, logical. Also, people seems to be better
at searching/recalling relevant existing knowledge.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Gabriel Dos Reis
And you are entitled to your belief :-)
And clearly there are at least as many interests as mathematicians.
As a trained differential geometer using formal systems to "algebraize"
topological and differential concepts, I am interested in the consequences
of the various formal axioms. For example, if I take a system that
tries to formalize (as an algebraic construction) the notion of limit [1]
and come to some formal rules where I can do lim(f/g) = lim(f)/lim(g),
it is not obvious a priori that the axiom 1/0 = 0 is entirely
inconsequential. One might wish it is inconsequential, but that is only
a wish or a belief and we hope our computation algebra systems do not
engage in wishful thinking.
[1] Michael Beeson and Freek Wiedij
"The meaning of infinity in calculus and computer algebra systems"
http://dx.doi.org/10.1016/j.jsc.2004.12.002
|
| Coming back to 'exp(-1/x^2)': with '1/0 = 0' this function
| formally is discontinuous. Informal reaction is that
Formal computer systems do not have "informal reactions".
If that expression is buried deep in some intermediary computation that
a human does not readily have access to, it is unlikely that one would
"informal" react in a timely manner to assess whether that formal or
informal continuity would affect the rest of the computation or not.
| you either have wrong definition or ask wrong question
| (note that informally uniteresting question is a kind of
| wrong question). The point is that sometimes you do not
| care what happens at zero and then '1/0 = 0' "works",
| sometimes you care, then one has to do definition via
| cases.
and I think I asked
# what parts of the usual classical theorems remain true and to what
# extent?
| > | apparently at least one such set of theorems (that of Isablelle/HOL)
| > | already uses this convention, so you will have to "patch"
| > | existing theorems when you want different convention.
| > |
| > | > The notion that "it is done in Isabelle/HOL therefore it must be right"
| > | > has to be tempered with the fact that Isabelle/HOL is a=20
| > | > *logical framework* in which one develops logics. What is often left
| > | > under-appreciated is that there are -many- logics used to prove this and
| > | > that theorem, but we don't have yet a coherent set of logics to
| > | > handle all that has been accomplished in computational mathematics.
| > | > Of course, if you are into Calculemus, you already know this.
| > | >
| > |
| > | As I wrote in another message: there is no _logical_ problem
| > | with 1/0 being 0.
| >
| > I don't think I ever suggested there is a fundamental logical problem
| > with 1/0 - 0. However, what I do suggest is that I've not yet seen a
| > single logical framework that contains all the "conventions" (that make
| > some proofs go through nicely, even if they are not conventional)
| > in a single place that handles Real Analysis. I've seen bits and pieces.
|
| I do not think you will find a single logical framework that directly
| contains all popular conventins.
Notice that I am not talking about notation conventions, but definitional
conventions. I do not know how you measure "popular conventions", but I
would go with the conventions in Bourbaki adaquately amended by
Geddes et al, as a start.
| IMHO various conventions are more
| like macros in programing languages: they are created to fit
| single problem (or domain) and are too specialised to work in
| general.
I have the odacity to believe that the definitional conventions by
Bourbaki is more that just "macros in programming languages" created to
fit single problem or domain and are too specialised to work in general
:-)
| Logical framework may (and probably should) contain
| a preprocessor to expand statements into canonical form. One
| can imagine predefined "macro files" with conventions for
| various domains.
|
| Let me add that IMHO when talking about logical framework for
| some part of mathematics like Real Analysis one needs mechanical
| checking (people are resonably good at inventing and writing
| down proofs, but formal checking is too tedious for them).
absolutely.
| And doing Real Analysis really means doing all mathematics.
I would not go as far as saying "all mathematics".
Bourbaki left a good part of geometry from its treatment of Real Analysis.
| AFAICS current checking systems are limited. One problem
| is that to give short proof one needs large volume of
| preexisting knowledge (theorems). Connected problem is
| that proofs encoded in procedural systems are hard to
| read for even for specialists. Some people seem to believe
| that if we keep encoding existing theorems in existing
| systems then eventually system will have enough "base
| knowledge" to allow writing real research results.
:-)
| I somewhat doubt this: IMHO proof checking systems
| should process mathematics in smarter ways.
we all agree; getting there, however, is distinctly non-trivial.
Our conventional practice of mathematics is highly ambiguous -- it
always amazes me that we manage to get through.
I learnt quite a few things from an experiment conducted with
colleagues: mechanization of the operational semantics of some advanced
object oriented programming language features. I learnt quite a few
things from that experiment
http://parasol.tamu.edu/~gdr/C++/layout/popl11.pdf
http://gallium.inria.fr/~tramanan/cpp/object-layout/
* Technologies available in modern PA/ATP systems are quite
advanced -- compared to the bad press they occasionaly get.
But we have a long way to go.
* Proof intended for machines is no proof intended for humans. :-)
| It seems
| that when dealing with logic current systems are
| more capable than humans. But humans works at many levels:
| pragmatics (what is doable and what is intersting),
| procedural, logical. Also, people seems to be better
| at searching/recalling relevant existing knowledge.
Sure.
Waldek Hebisch
> On Wed, Apr 13, 2011 at 9:22 PM, Waldek Hebisch <heb...@math.uni.wroc.pl>w=
> rote:
>
> > BTW: If you send me (via private mail) output of
> >
> > make > mlogg
> >
> > I should be able to tell you which command is responsible for
> > failure and how to debug this failure.
> >
>
>
AFAICS the problems begin here (in line 175447):
bash-3.2$ grep -nC 4 'missing separator' log.make
175443- cp $A.NRLIB/$A.fas /Users/jjgarcia/build/fricas-cvs/target/i686-apple-darwin10.7.3/algebra/$A.fas || exit 1 ; \
175444- done ; \
175445- touch stamp-bootstrap ; \
175446- fi
175447:boot.mak:2: *** missing separator. Stop.
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
175448-;;; Loading #P"/Users/jjgarcia/soft/ecl.st/lib/ecl-11.1.1/cmp.fas"
175449-Starting interpsys
175450-spad = "/Users/jjgarcia/build/fricas-cvs/target/i686-apple-darwin10.7.3"
175451- Using local database ./r7/algebra/compress.daase.. Re-reading compress.daase Using local database ./r7/algebra/interp.daase.. Re-reading interp.daase
The 'boot.mak' makefile contains command which do important compilation
step. If that is skipped, then one should expect errors later.
'boot.mak' is created in 'stamp-bootstrap' rule in 'src/algebra/Makefile.in'.
On my machine the first line in 'boot.mak' is quite long (23 kb), the
second one is pretty ordinary rule. It should look like:
main-bootstrap: A1AGG.NRLIB/A1AGG.lsp ..... (about thousend other files)
A1AGG.NRLIB/A1AGG.lsp: A1AGG.spad
echo ")compile" $< | DAASE=./r7 AXIOM=/home/hebisch/fricas/axp16/ax-buil
d29/target/x86_64-unknown-linux /home/hebisch/fricas/axp16/ax-build29/build/x86_
64-unknown-linux/bin/interpsys
So one should check if 'src/algebra/boot.mak' looks OK. Maybe 'make'
chokes on long line? Maybe 'echo' commands in 'src/algebra/Makefile.in'
produced wrong output? In particular I use 'echo -e '\techo...' to
get tabs into 'boot.mak'
Hope helps.
--
Waldek Hebisch
heb...@math.uni.wroc.pl