taskSavannah Administration - Tasks: task #14427, Submission of MetaLogic Inference


task #14427: Submission of MetaLogic Inference

Submitted by:  Hans Åberg <haberg>
Submitted on:  Tue 28 Mar 2017 01:50:21 PM UTC  
Should Start On:  Tue 28 Mar 2017 12:00:00 AM UTC Should be Finished on:  Fri 07 Apr 2017 12:00:00 AM UTC
Category:  Project Approval Priority:  5 - Normal
Status:  Done Privacy:  Public
Percent Complete:  0% Assigned to:  Ineiev <ineiev>
Open/Closed:  Closed Effort:  0.00

Add a New Comment (Rich Markup)

You are not logged in

Please log in, so followups can be emailed to you.


( Jump to the original submission)

Fri 31 Mar 2017 06:45:57 PM UTC, comment #8: 

Thanks! It works now: it was the first item that was omitted, the GIT option, and in addition, one has to wait some time for both GIT and the SSH key to be registered.

Hans Åberg <haberg>
Fri 31 Mar 2017 05:17:23 PM UTC, comment #7: 

First, you'll need to enable Git in your package configuration

Then, you'll need to register an SSH key in your account
and use it with Git
(you only use your password to login Savannah).

Ineiev <ineiev>
Site AdministratorIn charge of this item.
Fri 31 Mar 2017 04:46:16 PM UTC, comment #6: 

I decided (together with GNU Eval) to use GIT, but my password is not recognized using
  git push --all haberg@git.sv.gnu.org:/srv/git/metalogic-inference.git
So perhaps there is some initializing required.

Hans Åberg <haberg>
Thu 30 Mar 2017 03:33:45 PM UTC, comment #5: 

Thank you, approved.

Ineiev <ineiev>
Site AdministratorIn charge of this item.
Thu 30 Mar 2017 08:39:01 AM UTC, comment #4: 

For project name with you, not affecting the distribution and program names, then take metalogic-inference, as "metalogic" is normally spelled as one word (without hyphen) in English, which is also closer to the full name.

Hans Åberg <haberg>
Thu 30 Mar 2017 05:41:02 AM UTC, comment #3: 

Thank you; the distribution seems fine.

We'd prefer a more descriptive package identifier on Savannah (it doesn't really matter how your distribution tarballs will be named).

Ineiev <ineiev>
Site AdministratorIn charge of this item.
Wed 29 Mar 2017 09:52:38 PM UTC, comment #2: 

I made a new distribution; same URL as before:

The files with names starting with ._, MacOS (OS X) metadata (xattr) files, should now be removed. Copyright notice added to Readme.txt; examples/main.mli is an example file, and in addition, too short to be copyrighted. The files parser.output and examples/main.mlo are computer generated, were removed, but may otherwise not be copyrightable.

GNU Evaluation said the program name is fine.

Hans Åberg <haberg>
Wed 29 Mar 2017 02:00:50 PM UTC, comment #1: 

All distributed files, including ._src,
src/._Makefile.in, src/parser.output,
Readme.txt, examples/main.mli, examples/main.mlo,
should have valid copyright and license notices [0]; could you fix this?

Also, "mli" is a too short name; could you use something like

[0] https://savannah.gnu.org/maintenance/ValidNotices/

Ineiev <ineiev>
Site AdministratorIn charge of this item.
Tue 28 Mar 2017 01:50:21 PM UTC, original submission:  

A new project has been registered at Savannah
This project account will remain inactive until a site admin approves or discards the registration.

Registration Administration

While this item will be useful to track the registration process, approving or discarding the registration must be done using the specific Group Administration page, accessible only to site administrators, effectively logged as site administrators (superuser):

Registration Details

  • Name: MetaLogic Inference
  • System Name:  mli
  • Type: non-GNU software and documentation
  • License: GNU General Public License v3 or later (As per suggestion by the GNU Evaluation team, registered as non-GNU until formal approval.



The MLI program, short for MetaLogic Inference, proves statements, starting at the metamathematical level and up.

Other Software Required:

GMP; Flex and Bison if one wants to recompile the otherwise included parser.
GMP    LGPL v3 and GPL v2  https://gmplib.org
Bison   GLP v3 and LGPL  https://www.gnu.org/software/bison/
Flex     BSD  https://github.com/westes/flex

Tarball URL:


Hans Åberg <haberg>


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

Attach Files:

No files currently attached


Depends on the following items: None found

Items that depend on this one: None found


Carbon-Copy List
  • -email is unavailable- added by ineiev (Posted a comment)
  • -email is unavailable- added by haberg (Submitted the item)

    Do you think this task is very important?
    If so, you can add your encouragement to it.
    This task has 0 encouragements so far.

    Only logged-in users can vote.




    Follow 4 latest changes.

    Date Changed by Updated Field Previous Value => Replaced by
    2017-03-30 ineiev StatusIn Progress => Done
        Open/ClosedOpen => Closed
    2017-03-29 ineiev StatusNone => In Progress
        Assigned toNone => ineiev

    Back to the top

    Powered by Savane 3.5