Gabriel Dos Reis | 3 Jun 18:49 2011
Picon

[open-axiom-devel] 1.4.x branch and pending 1.4.0 release


Hi,

We are nearing the overdue release of OpenAxiom 1.4.0, hopefully by the
end of the weekend.  I create the 1.4.x branch for that purpose.
To check it out

   svn co https://open-axiom.svn.sf.net/snvroot/open-axiom/1.4.x oa-1.4.x

There have been lot of changes since 1.3.0.  I would like to get
OpenAxiom-1.4.0 out of the door soon.

The Windows platform build is moving toward a new GUI interface.  At the
moment, we have a basic GUI interface that still relies on the ASCII art 
display.  Graphics is not yet provided, but it is #1 item for 1.4.1.

The one thing that remains is the merging of Arthur's browser/server
interface to mainline.

Please test the 1.4.x branch and let me know of build problems or other
outstanding issues.  

(I'll be attending ISSAC 2011 in San Jose for those of you who would be
there.  There will be a poster and a paper presentation on on-going
automatic parallelization work based on OpenAxiom.)

Thanks,

-- Gaby

(Continue reading)

Gabriel Dos Reis | 20 Jun 19:57 2011
Picon

Re: [open-axiom-devel] Re: computation framework

Martin Baker <ax87438@...> writes:

[...]

| In other words they seem to be saying that the addition of either Law
| of the excluded middle or Double negation elimination have the same
| effect of converting intuitionistic logic to classical logic.

If you want to support intuitionistic logic, you cannot simplify
double negation.  See my comment in the definition of simplifyOneStep
in the package PropositionalFormulaFunctions1

  http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/boolean.spad.pamphlet?revision=2022&view=markup

-- Gaby

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev
Gabriel Dos Reis | 20 Jun 20:02 2011
Picon

Re: [open-axiom-devel] computation framework

Waldek Hebisch <hebisch@...> writes:

[...]

| To say this differently: --T = T but there are x such that
| --x ~= x.

Yep.  See simplifyOneStep in

   http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/boolean.spad.pamphlet?revision=2022&view=markup

-- Gaby

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev
Martin Baker | 20 Jun 20:11 2011

Re: [open-axiom-devel] Re: computation framework

On Monday 20 Jun 2011 18:57:22 Gabriel Dos Reis wrote:
> If you want to support intuitionistic logic, you cannot simplify
> double negation.  See my comment in the definition of simplifyOneStep
> in the package PropositionalFormulaFunctions1

Gaby,

So is boolean.spad.pamphlet general enough to support intuitionistic logic?

Martin

------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev
Gabriel Dos Reis | 20 Jun 20:38 2011
Picon

Re: [open-axiom-devel] computation framework

Martin Baker <ax87438@...> writes:

| On Monday 20 Jun 2011 18:57:22 Gabriel Dos Reis wrote:
| > If you want to support intuitionistic logic, you cannot simplify
| > double negation.  See my comment in the definition of simplifyOneStep
| > in the package PropositionalFormulaFunctions1
| 
| Gaby,
| 
| So is boolean.spad.pamphlet general enough to support intuitionistic logic?

OpenAxiom, and I believe all flavours of AXIOM, makes implicit use of
classical logic.  So, to avoid surprises, I assumed classical logic in
the simplifier.  However, for that particular algebra, that is easily
fixed by removing the line

   (f1' := isNot f1) case F => f1' -- assume classical logic 

from simplifyOneStep.  If that is done then boolean.spad.pamphlet
is general enough to support intuitionistic logic.
I believe the rules that `dual' uses are OK.

A long time ago, for the purposes of semantics-based program analysis, I
introduced the domain KleeneTrivalentLogic (also in
boolean.spad.pamphlet) which I views as a fairly good compromise
(from computational perspective).  Because of some misguided parser
simplifications (all flavours of AXIOM affected, OpenAxiom much less),
you have to be careful about how you write logical formulae with values
from the domain KleeneTrivalentLogic.

(Continue reading)

Игорь Пашев | 23 Jun 18:30 2011
Picon

[open-axiom-devel] Check for HyperDoc and others at runtime

Hi, All!


I'm trying to package Open Axiom for Debian
keeping Debian scheme to have separated
packages for separated programmes:

The problem is that Open Axiom package
can be installed without graphics or HyperDoc,
but OpenAxiom will try ro run them, infinitly
respawning its forks (they die because
there is no such file).

So I propose a wayt to detect presence of
additional programmes and do not start them,
if they are absent.
------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
Waldek Hebisch | 23 Jun 19:10 2011
Picon

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

Igor Pashev wrote:
> 
> Hi, All!
> 
> I'm trying to package Open Axiom for Debian
> keeping Debian scheme to have separated
> packages for separated programmes:
> http://packages.debian.org/source/sid/axiom
> 
> The problem is that Open Axiom package
> can be installed without graphics or HyperDoc,
> but OpenAxiom will try ro run them, infinitly
> respawning its forks (they die because
> there is no such file).
> 
> So I propose a wayt to detect presence of
> additional programmes and do not start them,
> if they are absent.
> 

It seems that you are packaging Axiom which is a different
project with different mailing list (axiom-developer@...).

--

-- 
                              Waldek Hebisch
hebisch@... 

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
Игорь Пашев | 23 Jun 19:12 2011
Picon

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

No, I'm packaging OpenAxiom :-)

2011/6/23 Waldek Hebisch <hebisch-o02PS0xoJP/hYjAhggEk4w@public.gmane.org>
Igor Pashev wrote:
>
> Hi, All!
>
> I'm trying to package Open Axiom for Debian
> keeping Debian scheme to have separated
> packages for separated programmes:
> http://packages.debian.org/source/sid/axiom
>
> The problem is that Open Axiom package
> can be installed without graphics or HyperDoc,
> but OpenAxiom will try ro run them, infinitly
> respawning its forks (they die because
> there is no such file).
>
> So I propose a wayt to detect presence of
> additional programmes and do not start them,
> if they are absent.
>

It seems that you are packaging Axiom which is a different
project with different mailing list (axiom-developer-qX2TKyscuCcdnm+yROfE0A@public.gmane.org).

--
                             Waldek Hebisch
hebisch-o02PS0xoJP/hYjAhggEk4w@public.gmane.org

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
Gabriel Dos Reis | 23 Jun 19:58 2011
Picon

Re: [open-axiom-devel] Check for HyperDoc and others at runtime

Игорь Пашев <pashev.igor <at> gmail.com> writes:

| Hi, All!
| 
| I'm trying to package Open Axiom for Debian
| keeping Debian scheme to have separated
| packages for separated programmes:
| http://packages.debian.org/source/sid/axiom
| 
| The problem is that Open Axiom package
| can be installed without graphics or HyperDoc,
| but OpenAxiom will try ro run them, infinitly
| respawning its forks (they die because
| there is no such file).

Hi Igor,

glad to hear from you.  I believe there was a bug in OpenAxiom-1.4.0
in that it did not build viewman but would try to spawn it.  That had
been fixed since then and the fix is part of the next OpenAxiom-1.4.1
release (hopefully, before the Sunday.)

| So I propose a wayt to detect presence of
| additional programmes and do not start them,
| if they are absent.

I agreed.  Usually, we detect at configure time whether the host has
X11.  Then at use time, we refuse to start the graphics component if
user requests it.  There was a glitch when I added a new GUI interface
for Windows platforms.

Could you test the 1.4.x branch and tell me whether you still see the
problem?  Thanks!

-- Gaby

------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
Игорь Пашев | 23 Jun 21:39 2011
Picon

Re: [open-axiom-devel] Check for HyperDoc and others at runtime



23 июня 2011 г. 21:58 пользователь Gabriel Dos Reis <gdr-wlZLyqSPnWSVc3sceRu5cw@public.gmane.org> написал:
 I believe there was a bug in OpenAxiom-1.4.0
in that it did not build viewman but would try to spawn it.  

Sure, I caught it (SVN revision r2117).

As for Debian, I'm building r2199 now.

And I'm talking about src/sman/sman.c:
function start_the_graphics:
it tries to start viewman even if it does not exist
(in Debian, Axiom and OpenAxiom are built with X support,
but all graphics stuff is in the separated package and may not be installed).

So, since viewman does not exist, the forked process dies and
its parent respawn it again and again.

I believe it can be changed to something like this:
if (start_graphics && graphics_present)         start_the_graphics();

Does it make sense?
------------------------------------------------------------------------------
Simplify data backup and recovery for your virtual environment with vRanger.
Installation's a snap, and flexible recovery options mean your data is safe,
secure and there when you need it. Data protection magic?
Nope - It's vRanger. Get your free trial download today.
http://p.sf.net/sfu/quest-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@...
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Gmane