taskSavannah Administration - Tasks: task #3924, Submission of Isar Mathematical...

 
 

task #3924: Submission of Isar Mathematical Library

Submitter:  Slawomir Kolodynski <slawekk>
Submitted:  Wed 23 Mar 2005 11:54:02 PM UTC
   
 
Should Start On:  Wed 23 Mar 2005 12:00:00 AM UTC Should be Finished on:  Sat 02 Apr 2005 12:00:00 AM UTC
Category:  Project Approval Priority:  * 5 - Normal
Status:  Done Privacy:  Public
Assigned to:  zeus Open/Closed:  Closed
* Mandatory Fields

Add a New Comment Rich Markup
   

Sat 23 Apr 2005 04:26:00 PM UTC, comment #3: 

Hi,

Apologize for the delay in my answer, I didn't see your answer on my
email account, sorry.

I have approved your project.  You will receive an automated e-mail
containing detailed information about the approval.

Regards.

Jonathan Gonzalez V. <zeus>
Wed 06 Apr 2005 04:26:39 PM UTC, comment #2: 

Jonathan,
Thank you for reviewing my code.

>you had licensed the
> 'Fol1.thy' file
> under the GNU GPL, did you already know it?


No. It was my intention to license everything under the modified BSD license.

>if you
> do not have
> problems with this point, we can approve your
> project


I understand the suggestion.
Unfortunately, the auhors of Isabelle (the theorem prover my project depends on) made a mistake of licensing their software under the modified BSD license. I have made a reluctant decision to use the same license to allow the code to flow freely between my project and Isabelle without any licensing issues, real or imaginary.
If none of my code is included in the official Isabelle distribution during the first year of my project's public existence I will change the license to GPL. I plan to require the contributors (if any) to give me a permission in advance to do that.

I hope my project will still get approved, even though its license is not the best for free software.

Regards,
Slawomir

Slawomir Kolodynski <slawekk>
Wed 06 Apr 2005 01:19:00 AM UTC, comment #1: 

Hi,

I'm evaluating the project you submitted for approval in Savannah.

I reviewed your source code and you had licensed the 'Fol1.thy' file
under the GNU GPL, did you already know it? if you do not have
problems with this point, we can approve your project, please let us
know about your decision.

Regards,

Jonathan Gonzalez V. <zeus>
Wed 23 Mar 2005 11:54:02 PM UTC, original submission:  


Site Admin. Approval/Edition URL:
 <https://savannah.gnu.org/admin/groupedit.php?group_id=7455>


###### ORIGINAL SUBMISSION DETAILS ######

System Group Name:
-----------------
  isarmathlib


Full Name:
----------
  Isar Mathematical Library


Type:
-----
  non-GNU


License:
--------
  Modified BSD License


Other License:
--------------



Description:
------------
  The goal of the project is to create a library of formalized mathematics, written for the Isabelle/Isar theorem prover.
In formalized mathematics definitions and theorems are written in a computer language (Isar in this case) so that they can be verified by a machine.

Preliminary sources of the IsarMathLib project can be found at
http://www.skokodyn.com/IsarMathLib/ .

For some background on formalized mathematics I suggest
ftp://ftp.mcs.anl.gov/pub/qed/manifesto



Other Software Required:
------------------------
  The project depends on the Isabelle/Isar theorem prover
(http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html),
distributed under the BSD license.




Other Comments:
---------------


#########################################

Slawomir Kolodynski <slawekk>

 

(Note: upload size limit is set to 16384 kB, after insertion of the required escape characters.)

Attach Files:
   
   
Comment:
   

No files currently attached

 

Depends on the following items: None found

Items that depend on this one: None found

 

CC list is empty

 

There are 0 votes so far. Votes easily highlight which items people would like to see resolved in priority, independently of the priority of the item set by tracker managers.

Only logged-in users can vote.

 

Follow 5 latest changes.

Date Changed by Updated Field Previous Value => Replaced by
2005-04-23 zeus StatusNone Done
    Percent Complete60% 100%
    Open/ClosedOpen Closed
2005-04-06 zeus Percent Complete0% 60%
    Assigned toNone zeus

Back to the top

Powered by Savane 3.13-4b48.
Corresponding source code