You first need to get an account on sourceforge.net. See the SourceForge documentation for how to register for a user account.
Then, once you are on SourceForge as a developer, you should send email to one of the project administrators and ask to be added as a developer. It will help if we either know who you are already or have received patches or bug fixes from you in the past. (You can do the latter using SourceForge read-only access.) But don't be shy.
When you have gotten your SourceForge account, you next need to get ssh to work to SourceForge. The first thing to do is to read the documentation from SourceForge about it. In particular, read the document Guide to Generation and Posting of SSH Keys from the SourceForge documentation. (If you plan to use Eclipse, don't use PuTTY to generate the keys.) In particular, you will need to upload your ssh keys to avoid having to retype your password when you are working with CVS. Note that you have to wait some time before these take effect.
Also, while you're working on your SourceForge account, you should sign up for all the mailing lists for the jmlspecs project (except that you only need to sign up for either the jmlspecs-interest list or the for the jmlspecs-release list; signing up for both isn't necessary). You should also sign up for both of the mailing lists for MultiJava project, since JML is build on top of MultiJava.
If you are going to commit files to either project, then you should sign up for the mailing lists jmlspecs-commits and multijava-commit using your @users.sourceforge.net account. This is because commit messages are sent out by your sourceforge.net user account, and we only allow subscribed users to send such messages. (For other mailing lists, you can sign up from whereever you want to send messages from.)
There are currently several "projects" within the JML effort.
If, however, you are working on one of the newer efforts, follow the brief instructions in the following items, see the documentation contained therein, and ignore the rest of this document.
To use CVS to check out the MultiJava sources first do (in bash)
export CVS_RSH=ssh
or in csh or tcsh:
setenv CVS_RSH ssh
Then to get a checkout of the MultiJava and JML sources, do the following, where yoursflogin should be substituted with your source forge login name.
cd ~
cvs -z3 -d:ext:yoursflogin@multijava.cvs.sourceforge.net:/cvsroot/multijava checkout -P MJ
cvs -z3 -d:ext:yoursflogin@jmlspecs.cvs.sourceforge.net:/cvsroot/jmlspecs checkout -P JML2
Note the use of the -P flag to cvs checkout, this prunes directories that are not needed.
Documentation for JML is hosted separately in Subversion, and can be retrieved with the following command.
cd $HOME
svn checkout https://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs/documents/trunk JMLdocuments
After all files have been retrieved, you will need to add several symbolic links, which can be done as follows. If you see errors when trying to build JML2's documentation, one or more of these links is probably missing. This process assumes you keep MJ and JML2 in $HOME; if not, substitute the appropriate directory in the first line below.
cd $HOME
cd JML2/org/jmlspecs
ln -s ../../../JMLdocuments/org/jmlspecs/samples .
cd ../../
ln -s ../JMLdocuments/docs .
cd ../JMLdocuments
ln -s ../JML2/Make.ProjDefs ../JML2/raccompiled ../JML2/nonFraccompiled .
cd org/jmlspecs
ln -s ../../../JML2/org/jmlspecs/models .
ln -s ../../../JML2/org/jmlspecs/lang .
If you have an old checkout of JML2, then you should first do a make cleanall and then do a cvs update -P; this will get rid of the old
(If you want to update the JML web pages, you can do so by using the following command, with the same convention about yoursflogin as above.)
cvs -z3 -d:ext:yoursflogin@jmlspecs.cvs.sourceforge.net:/cvsroot/jmlspecs checkout -P web
You need to set up your CLASSPATH environment variable, and export it. This must contain the directories with jar or class files for MultiJava, JML2, ANTLR, JUnit, and GNU getopt, and the JML specs directory. At Iowa State, we put the JML2 directory in our home directory, so it's path is ~/JML2. We keep Java's J2SDK in /usr/local/jdk1.4.
If you don't have Java's J2SDK installed, you can download it from http://java.sun.com. You need at least a 1.4.1 J2SDK (although 1.4.2 is recommended). Be sure to also install the documentation underneath the Java install.
It's possible to build and test everything except jmldoc and mjdoc with J2SDK 1.5 (Java 5). To do this, you have to define the name JAVA5, and export it. For example in Bash, do the following.
export JAVA5=1
If you don't have ANTLR installed, you can download it from http://www.antlr.org. You need ANTLR version 2.7.4 or later. (We have tested with versions 2.7.6 and 2.7.7.) We keep ANTLR in /usr/local/antlr. When you install Antlr, you have to make the javadocs for Antlr, for example by running the make-antlr-javadocs-unix or make-antlr-javadocs-cygwin scripts in the bin-for-developers directory.
If you don't have GNU Getopt installed, you can download it from
http://www.urbanophile.com/arenn/coding/download.html. We installed the
package under /usr/local/gnu; note that this means that
/usr/local/gnu will contain a subdirectory also named gnu.
In the end you will have a directory
/usr/local/gnu/gnu/getopt/ containing the
Java files in the GNU Getops release. (Note the gnu/gnu in
the path above.)
You'll have to go into that directory and do make all docs
to build it.
If you don't have Junit installed, you can download it from http://www.junit.org. You need at least version 3.8.1. (For versions prior to 3.8.1, you may have to unjar the src.jar file in it, and you will also need to take out the deprecated "assert" methods from "junit.framework.Assert", and instead use the assertTrue method). We keep Junit in /usr/local/junit. The release of JUnit is already compiled, so simply unpacking it is enough.
You may also want to get Ant, and install
it under /usr/local/ant.
With all of the above, you will want to have the following in your .profile file (for sh or bash):
export CLASSPATH=".:$HOME/MJ:$HOME/JML2:/usr/local/antlr/antlr.jar:/usr/local/junit/junit.jar:/usr/local/gnu:$HOME/JML2/specs:/usr/local/jdk1.4/lib/tools.jar"
Either you need to have /usr/local/jdk1.4/lib/tools.jar in your CLASSPATH, or you can follow the directions in the JML README.html file about copying your tools.jar file to the jre/lib/ext directory. This is for mjdoc and jmldoc. It's also important to have the MJ directory listed before the JML2 directory in your CLASSPATH; this can help prevent some subtle problems if you accidently forget to recompile in the MJ directory after making a change, such as committing a file, and then a compilation from within JML2 emits a .class file in a directory under JML2.
If you use csh or tcsh, change your .login file instead to something like:
setenv CLASSPATH ".:$HOME/MJ:$HOME/JML2:/usr/local/antlr/antlr.jar:/usr/local/junit/junit.jar:/usr/local/gnu:$HOME/JML2/specs:/usr/local/jdk1.4/lib/tools.jar"
You'll need to use GNU make to use the make system. On Linux (and cygwin) this is automatic, but on some machines you'll need to need to write a shell script that redirects make to gmake. You might have the following in a shell script that is in your file ~/bin/make, assuming that is in your path before the usual version of make (/bin/make). (Also, take out the spacing before each line.)
#!/bin/sh exec /usr/local/bin/gmake "$@"
In the directory above this one (i.e. in $HOME/JML2), the file Make.ProjDefs and the Makefile have a bunch of useful targets. There are even more useful targets in the MultiJava directory's file Make.Defs. These are included by all the makefiles.
If you're using the latest version of cygwin or Linux, their jar command causes the jmlrac tests to fail one test (BootClassDownCall.java). If this happens to you, write a script named jar, like the one for make suggested above, that maes sure that runs the jar command from the JDK, and put it in your PATH before the bad one in /usr/bin/jar. (A sample is availble at http://www.eecs.ucf.edu/~leavens/Windows/bin/jar.)
The makefiles use several environment variables, which you need to set. The easiest way to do this is to make a copy of and edit one of the following files, in JML2/bin-for-developers:
Let's assume you make a copy of this in ~/bin/jml-sourceme.sh. You need to check all of the variable definitions in ~/bin/jml-sourceme.sh. You also need to source (not just execute) this file before starting to work with the JML make system.
It's possible to work with the JML sources from Eclipse. Because we build from makefiles, if you check out MJ and JML 2 as Java projects, go to the Project menu, then Properties, then Builders, then uncheck the Java builder checkbox. (Ignore the warning message.) You'll have to ignore various errors that occur because some files are not generated and ignore errors from testcases (that are supposed to be errors). You can also, if you wish check it out as a non-Java project, to avoid some of these problems. To build, use make, as described below, instead of letting Eclipse build them. You will also want to use a version of the following sourceme file:
When using Eclipse, don't check your .project file into CVS.
In theory, you shouldn't need to have a separate sourceme file for the MultiJava project, but if you are regenerating the Javadoc comments for MultiJava, you will need to use one like the example sourceme files in the MJ/bin directory.
To begin work, after following the steps above, and then source-ing your file ~/bin/jml-sourceme.sh.
source ~/bin/jml-sourceme.sh
Now do the following to compile a version of JML and to get the HTML files generated.
cd MJ
make rebuild-all
cd JML2
make rebuild-all jmldocs html
The rebuild-all target first does a make pristine and then makes the build target. Both of these are useful on their own. You can also shortcut all of the above by doing make everything+.
A handy shell script, makeboth, is included in the bin-for-developers directory. This script executes make, first in the MJ directory and then in the JML2 directory, using any arguments given to the script as arguments to make.
When you are working with your own version of JML, it's important to have a shell script in your PATH that runs your version of the checker, not the standard one. For this reason, the JML2/bin-for-developers provides scripts with a suffix "2" at the end. You can thus copy the appropriate versions of these into a directory you own on your PATH. For example, if you are using cygwin, copy the scripts jml2-cygwin, jmlc2-cygwin, jmldoc2-cygwin, junit2-cygwin, and jtest2 to your personal bin directory, renaming them as jml2, jmlc2, jmldoc2, jmlrac2, jmlunit2, and jtest2. This can be done automatically from the makefile in JML2, for example by executing the following on cygwin:
cd ~/JML2
source ~/bin/jml-sourceme.sh
make INSTALLTYPE=cygwin install-developers-scripts
You may possibly need to edit your copies of these scripts, especially if you don't keep the JML2 directory in your home directory.
JML is open source software. New files should have the appropriate GPL comment in the style of org/jmlspecs/copyright-for-java.txt or org/jmlspecs/copyright-for-make.txt (see the bottom of this file). For the specifications for libraries we use the LGPL instead; see the specs directory for examples.
If you use emacs, when working with antlr files, put the following in your .emacs file to convert tabs to spaces. This will help people who don't use emacs :-).
;;; ANTLR mode
(autoload 'antlr-mode "antlr-mode" nil t)
(add-to-list 'auto-mode-alist '("\\.g\\'" . antlr-mode))
(add-hook 'speedbar-load-hook ; would be too late in antlr-mode.el
(lambda () (speedbar-add-supported-extension ".g")))
(add-hook 'antlr-mode-hook
(function (lambda ()
(make-local-variable 'indent-tabs-mode)
(setq indent-tabs-mode nil))))
When you commit changes, it is important to first test your changes to make sure you aren't breaking any other code or tests. The basic testing strategy is the following:
cd ~
cvs -q update -d -P MJ JML2
cd JML2
make rebuild-everything quiet-tests
If you changed anything in the MultiJava project, you need to build and test those changes as well. Since mjc is used to compile JML, you should build and test the MultiJava changes first. The basic testing strategy in this case is:
cd ~
cvs -q update -d -P MJ JML2
cd MJ
make rebuild-all quiet-tests
cd JML2
make rebuild-everything quiet-tests
Alternatively, if you have configured the makeboth script, you can use
cd ~
cvs -q update -d -P MJ JML2
makeboth rebuild-all quiet-tests
This 'makeboth' approach has the advantage that the compilation and test results will be written to the file results.out in your home directory. This makes it easier to scan through the results of testing and check for any errors.
Of course, you don't always need to run all the tests during development, and if you can be sure that the tests aren't going to fail because you know your changes are localized, then you can go ahead and commit them before doing all of this testing. Still it's a good idea to test as described above whenever you have time (e.g., when you're sleeping :-).
In general, for each feature you add to the software, there should be tests that exercise it, so that others will not break your code when they make changes.
The following is no longer much relevant, except for the PLSL module. The PLSL module is a replacement for all of ANTLR, JUnit, and GNU getopt. If you use this module, you don't need such a complicated CLASSPATH, and can instead set your CLASSPATH as follows (for sh or bash users):
export CLASSPATH=".:$HOME/MJ:$HOME/JML2:$HOME/PLSL:$HOME/JML2/specs:/usr/local/jdk1.4/lib/tools.jar"
To use CVS on larch, if you use bash (or sh) as your shell, put the following line in your .profile file:
export CVSROOT='/home/larch/research/master'
or if you use tcsh (or csh) as your shell, instead put the following in your .login file:
setenv CVSROOT '/home/larch/research/master'
Then do the following
cd ~
cvs checkout -P PLSL
The -P flag says to prune out directories that aren't needed.
When you want to update your copy, you can do that by running
cd ~/PLSL
cvs update -d -P
More information on CVS can be found from the info documentation, which you can reach in emacs by running the help, selecting browse manuals in info (i), unsupported, and then CVS. It is also on the web, for example at http://durak.org/cvswebsites/doc/.
Be sure that your umask is not set to deny group read or execute permissions. For example, put
umask 002
in your .login file.
It's best if you do your work while in the "jml" group, by executing
newgrp jml
before your begin work. It's absolutely critical that you do this if you are committing files, especially new files.
If you commit a new directory, the scripts should change it to the "jml" group after a while. If this doesn't happen, you can change it yourself by doing the following (and ignore error messages about files you don't own).
cd $CVSROOT/JML2
chgrp -R jml .
chmod -R go+r .
find . -type d -exec chmod ug+w '{}' ';'
You might want to put that in a shell script and run it after committing files. Doing that is important if you use CVS remotely from a machine other than larch.
To work remotely on the machine "pvs", on that machine put the following in your ~/.bash_profile file.
CVSROOT=":ext:larch.cs.iastate.edu:/home/larch/research/master"
CVS_RSH=ssh
export CVSROOT CVS_RSH
If you use csh or tcsh, use instead of the above the following:
setenv CVSROOT ":ext:larch.cs.iastate.edu:/home/larch/research/master"
setenv CVS_RSH ssh
You'll also need to set up ssh so it works from pvs to and from larch.
It doesn't seem to work to manipulate the CVS repository through samba. The problem is that file names get turned to all lower case.
Thanks to the JML team at ISU, especially to Curtis Cliftion for help with these tips. Thanks to Patrice Chalin and others for help in getting them to be more useful elsewhere.
Please let Gary Leavens know of any other tips you think are helpful for this work.
@(#)$Id: developer-tips.html,v 1.50 2008/01/09 16:12:10 leavens Exp $
Copyright (C) 2002-2006 Iowa State University
This file is part of JML
JML is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version.
JML is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with JML; see the file COPYING. If not, write to the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.