Distribution of starting files for assignements and assignment submission will be organized through Git Hub. You need to complete the following steps:
Logika is a program verifier and a natural deduction proof checker for propositional, predicate, and programming logics. Logika is part of a much larger analysis and verification framework developed by Robby called Sireum.
It is crucial that you get set up to use Logika during the first week of class. We will use Logika every week in class, and almost all homework assignments will use it.
You will need to setup the Sireum IVE (Integrated Verification Environment) which contains Logika.
Logika can be used in a nice IntelliJ-based Integrated Verification Environment (Sireum/Logika IVE) (this is what we recommend for doing all your classroom exercises and homework).
The general steps for installation are:
When watching the above videos, you will to perform the following downloads:
After completing the instructions in the videos, you should check that you have a java run time installed (“java -version” at a command prompt will tell you the version of java installed). If your version is 1.8.0_144 or older you will need to update the Java installation before continuing.
By following the videos above in order, you should be able to “install” the Sireum IVE and integrate the examples project. You may notice a lot of instructions on the Sireum Installation page. These steps are not necessary–Do not follow them as they may contain obsoltete information.
It is normal to see modal dialog boxes asking you to choose settings
NOTE for Mac users. The videos are for windows. You will also need to:
Creating New Projects/File
The examples and homework come with project structures and files already created. However, there’s a good chance that you will want to create your own project/files from scratch to work on examples in class or to solve FTYD exercises. Here’s a video that shows you how you can create an empty project and an empty file to work on such examples.
While several “Desktops” (the computers in 1118, 1117, 1114) have a Sireum icon in their applications lists, conflicts between the Summer’s hardware, architecture and Sireum updates have not been been resolved and these “links” will not work. As of 16 August your best bet to install Sireum on departmental resources is to install it on your CIS remote windows desktop.
The Department is working to resolve these issues.
Installation of Sireum IVE on the CIS Remote Windows Desktop(RWD).
ONCE YOU HAVE INSTALLED SIREUM, DO NOT UPDATE INTELLIJ! Intellij will occasionally give you pop-ups sying a new version is available and press to update. Ignore these. Sireum will not be rolled to a new version of Intellij until Summer 2019 and most likely WILL NOT WORK with “upgraded” versions. If you update Intellij and Sireum breaks, you will have to reinstall Sireum.
Z3 is a high-performance Satisfiability Modulo Theories (SMT) solver being developed at the Research in Software Engineering (RiSE) group in Microsoft Research.
We will use Z3 early in the course and then we will refer to it throughout the rest of the course. There is a web-based Online version which you will use to verify your homework.
Our use of Git and GitHub is intended to familiarize you with the steps necessary to manage a single branch repository that is synchronized between the “official” remote repository and one or more local copies of that repo. From the command line, you are expected to be able to:
To facilitate local-to-remote repository communication. We suggest you set up SSH keys on the computers you use and register them with Github.
If you choose to work with multiple local repositories (say one on your personal computer hard drive and another on a USB you carry), you are responsible for synchronizing them. You will need to use the Git pull command to update each local repository to the “state” that remote is in BEFORE you start working in the local repository.
Standard work flow – Ensure your local repo is up to date with the remote
If you:
THEN your local is up to date If you need to make a new local repo, clone the remote to your machine.
If you are not sure that the local matches the remote, or you know it does not,
Standard work flow – Commit your changes to the local repo
Standard work flow – Push your changes to the remote
Optional : Check the Github site for the commit
Standard work flow – Cloning
Occasionally you may need to make a new copy the remote repo. This could be because you are working from a different computer. It could be because something has gone terribly wrong with your existing repo and it will not commit or push to GitHub (very rare). When you need to create a new local repo:
Standard work flow – If your local repo stops working with GitHub
In past semesters some students have experienced problems where their local repo stopped communicating GitHub. Inevitably, this occurs when one needs to push a big commit, like an entire homework, and it is close to the due-time.
First try making a “new-local”, then copy-replace the changed files from the “old-local” to the “new-local”. Git add, commit and push. This generally fixes the problem as the “corruption” is typically in hidden .git files not in the user content files.(Be sure to delete the “old local”).
If there are still problems, you may have an expired credential. The solution is to make a new credential (SSH key, token, saved password, etc.). We cannot guess which type of credential has expired and are not experts at their creation; you will have to figure this out.
Finally, you can upload files and edit files directly via the GitHub web interface. This should be your last resort. You will need to commit your changes and remember to clone the new commit(s) to a new local directory.
Students are free to integrate Git with Intellij or any number of third party apps (GitGui, GitExtensions, etc). The TAs can offer limited-to-no help on using these tools. As students, you are responsible to know the commands for cloning, adding files/changes, committing and pushing for your local repository.