Roger Bishop Jones wrote:
...

We could have one directory for such things, with subdirectories for each "contribution" and some rules for these to permit a uniform and simple way of installing whatever selection a user wants to make use of, and then have different top level directories for things which don't fit into that.

Perhaps one directory for "maths_eq"-like contributions, one for contributions in the form of patches, and another for other kinds of things. The first two having some rules to provide uniform installation, the last consisting of contributions each of which makes up its own rules.

That sounds flexible enough. Does this all go into one repository? (I don't know what is possible or most suitable using Mercurial on google code.)


Personally, I am happy with GPL (2 or 3).

Well, so far it looks like GPL3 on google with mercurial.

GPL 3 would rule out the ProofPower code base as that is GPL 2. GPL 2 and 3 are 'incompatible': http://www.gnu.org/licenses/rms-why-gplv3.html
So, whilst ProofPower is GPL 2, my preference would actually be GPL 2.
(Note ProofPower does not specify "any later version" regarding GPL.)

In fact, this may be an issue for the sort of contributions you are talking about too. On the one hand, one could view ProofPower like a compiler that processes theories and these theories could be viewed as works in their own right, so they could have whatever licence the author wants. On the other hand, one could view these theories as ML programs that make calls to the ProofPower library of ML functions so would need to be available under GPL 2:
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#IfLibraryIsGPL
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#LinkingWithGPL
That does not stop them also being made available under a 'compatible' licence, i.e. one that is upstream from GPL 2 in the following diagram:
http://www.gnu.org/licenses/quick-guide-gplv3.html#new-compatible-licenses
Under the latter interpretation, which is probably the right one, I don't think it would be possible to make the contributions available under GPL 3 as it stands.


On google you can have a different licence for documentation, one of the creative commons licences. Does anyone think that would be a good idea?

I don't know much about the creative commons licence - what are the benefits and drawbacks for documentation?


I have used Subversion on a few projects and found it too
 inflexible. Without access to the Subversion repository
 a number of things aren't possible.
 (Simply being
 connected to the internet doesn't necessarily solve
 this: in my case, the Subversion server was only visible
 from an internal company network.)

I don't understand the distinctions you are making here, and think that I need to.

 Whilst the
 Subversion working copy is local to a machine, without
 visibility of the repository I couldn't see the log of
 previous commits, nor make any commits.  Working on more
 than one commit was a pain.  (Sometimes, I found that a
 particular enhancement required a logically separate
 enhancement to be made first...) Fortunately the
 Git-Subversion interface worked quite well and I was
 able to use Git locally to prepare a series of commits
 and upload them once I was connected to the Subversion
 repository.

I'm not convinced that the problems you are experiencing reflect what would happen if we had a properly set up subversion repository.

For this I think you need to have the repository on a server which runs a subversion service. Having a repository which is visible across the network by other means is not the same. I have a subversion repository at rbjones.com, but cannot provide a general service because rbjones.com is on a virtual host so all access to the repository has to be through my username.

Sorry, all I was saying is that when one doesn't have access to the Subversion repository (for whatever reason), any operation that requires access to the Subversion repository won't work, which includes various operations that I would do normally during the course of development, e.g. looking at the previous log messages or previous revisions or making commits.

Wherever the repository is, or however it is set up, if you don't have access, you can get stuck. Whilst a repository on Google Code would be quite accessible, I do a lot of development on the move and wouldn't even want to be dependent on an internet connection.

With a distributed VCS, you have your own local repository, so access is not a problem.


Also I don't understand your commit problem, why was it desirable to have a series of commits rather than just one?

If I'm making three separate changes that are totally unrelated, it's better for these to be separate commits, in my view. For example, it is easier for people to understand the changes if they're separated out. Also, it would allow someone else to pull one of the changes into their development without having to get all three.


Well you and Rob are both against subversion so we can do Mercurial at google or Git at sourceforge, unless anyone prefers some other host.

I think Rob prefers Mercurial, which I'm quite happy with too.


Both of these are blocked for Cuba, Iran, Libya, North Korea, Sudan, Syria, does anyone think that important?

I haven't heard of anyone working on ProofPower in these countries...

Phil




_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to