The instructions in this page should help you setting up the KeY development environment for the HacKeYthon. In case of any problems, please contact Dominic Steinhöfel before the event. The goal is that every participant has a working development environment set up before the HacKeYthon.
General Instructions
- Download the KeY bootstrap archive. This archive contains the recommended file structure, a script for starting Eclipse with the right parameters, and a convenience script for Linux 64bit systems for performing most actions outlined in the following automatically.
- Extract the contents of the archive to the destination where you want your shiny new KeY workspace to appear, for instance in your home directory (such that you have the folder “key-workspace” in “/home/yourusername/”).
- Make sure you have Git installed on your system. For Windows, there is Git for Windows, on Debian-like systems, you can run “sudo apt-get install git” from a shell.
- Also make sure you have access to the KeY GitLab. You should furthermore have created an SSH key on your system which you registered there. Instructions are available at the GitLab help page (sections “Generating a new SSH key pair” and “Adding an SSH key to your GitLab account”).
Download Eclipse, Check Out the Git Repository, Install Plugins, Import Projects
The following subsections are mutually exclusive; please choose the one that applies to you.
Linux 64 bit, Script [recommended]
- Run the script “setup.sh” by calling “./setup.sh” from the command line in the directory to which you unzipped the archive.
Manual Process
The following instructions should apply to all operating systems. Windows users should interpret “/” as “\” for the directory separators.
- Download the “Eclipse IDE for Java Developers” package which applies to your system from the Eclipse download page.
- Extract the contents of the archive to “key-workspace/Tools/eclipse/”. Inside this directory you should find the Eclipse executable.
- Change to the directory “key-workspace/GIT/”.
- There, run “git clone git@git.key-project.org:key/key.git”.
- Open eclipse via the scripts “eclipse” or “eclipse.bat” (Windows) in the directory “key-workspace/Development/KeY/eclipse”.
- Install the following plugins via “Help > Install New Software”, selecting the update site “2018-09 – http://download.eclipse.org/releases/2018-09”:
- “EMF – Eclipse Modeling Framework SDK”,
- “OCL Classic SDK: Ecore/UML Parsers,Evaluator,Edit”,
- “Graphical Modeling Framework (GMF) Runtime SDK”,
- “GEF Common SDK”,
- “SWTBot for Eclipse Testing”,
- “SWTBot for GEF Testing”,
- “SWTBot for SWT Testing”,
- “SWTBot IDE Features”,
- “Graphiti (Incubation)”
- Restart when prompted.
- Import all KeY eclipse projects via “File > Import > General > Existing Projects into Workspace”, selecting “key-workspace/GIT/key/” as the root directory (choose “Select All”).
Troubleshooting Compilation errors
Please open eclipse via the scripts “eclipse” or “eclipse.bat” (Windows) in the directory “key-workspace/Development/KeY/eclipse”. You might encounter various compilation problems that I try to address in the following.
Since you imported all projects (either automatically or manually), there will also be the project “BankJML” which shows various errors. Just remove it (without deleting it from the workspace), you won’t need it.
In the class “JDTUtil”, you could observe an error like “Access restriction: The method ‘JavaElementLabelComposerCore.appendTypeLabel(IType, long)’ is not API …”. Resolve this by navigating to the problematic file, clicking on the error and choosing the quick fix (Ctrl + 1, “Configure Problem Severity”), clicking on “Configure Project Settings”, and then setting the rule for “Forbidden reference” to “Warning”. This should solve it.
If you are reported errors like missing projects “key.util” which are though not missing, try to remove the projects from the workspace (choose to not delete them from the disk) and importing them again (from the directory “key-workspace/GIT/”). Don’t import BankJML again.
If you encounter a compilation error in the “key.core.test” package, because of the missing folder “genSrc”, resolve this by moving to the directory “key-workspace/GIT/key/key/key.core.test/” and running “ant generateproofcollectionparser”. You can also run this ant goal via the eclipse ant view (Window > Show View > Other > Ant), then you don’t need to use the command line.
After and between those steps, try a “Project -> Clean” with “Clean all projects” set. You might have to run the aforementioned ant command again. Now you hopefully don’t see any more errors…
Code Convention Settings
Now, the time has come to apply some settings contributing to the conformance of your newly written code with the KeY coding guidelines.
Code Formatter
Open “Window > Preferences”, choose “Java > Code Style > Formatter”. In the dialog, choose “Import” for importing a new profile, navigate to “key-workspace/GIT/key/key/doc” and choose “KeYCodeStyle.xml”. I personally edited the style to allow for “on/off” tags in the code that are spared by auto formatting, such that commented out code or extraordinary code snippets with special formatting are not messed up. For that, choose “Edit”, “Off/on Tags”, “Enable Off/On tags”.
User Name in Comments
In the preferences dialog, go to “Java > Code Style > Code Templates”, choose “Comments > Types” there and edit the style by replacing the “${user}” placeholder with your real name (without German Umlauts or other special characters!).
Configure Auto Save Actions
There are some things which can automatically be done when saving which increase the code quality a little. In the preferences window, navigate to “Java > Editor > Save Actions” and check “Perform the selected actions on save”. Then check “Organize imports” and “Additional actions” (don’t check “Format source code”, since it’s bad for version control when you’re editing previously existing classes), and click on “configure”. In the appearing dialog, check “Remove trailing whitespace” and “Correct indentation”. Make absolutely sure that you don’t check “Sort members” since it’s a nightmare for version control. Everything else should be left as-is.
Click “Apply and Close” in the preferences window.
Run KeY and the Test Suite
Once you set up KeY, you should try to run the KeY GUI and the default test suite. For this, first open the class “de.uka.ilkd.key.core.Main” in the “key.ui” project and run it as a Java application; this should produce you the KeY GUI. After that, try out “de.uka.ilkd.key.suite.TestKey” in “key.core.test” (run as JUnit test suite).