Compiling and using Agda through the Windows Linux Subsystem

The Windows Subsystem for Linux (WSL) more or less runs a linux kernel on Windows 10. In this post, I will describe how to use WSL to compile and run Agda, a dependently typed functional programming language. Compiling agda yourself makes sense if you want to use the latest features, of which there are quite nice ones. The approach presented here is just my preferred way of compiling and using Agda on a Linux system with some minor adjustments.

Prerequisits for compiling

First, you need the “ubuntu app”, you can install it following this guide. Essentially, you just have to activate WSL and install the app through the Microsoft Store, but following the guide step by step allowed me to do it without creating a Microsoft account.
After installing your ubuntu app will ask you to create a new account and it will probably need some updating, which you can do by running:

sudo apt-get update

A usability hint: You can copy-paste to the ubuntu app by copying with CTRL-C and right-clicking into the ubuntu-window. You have to make the ubuntu-window active before the right-click. You can copy stuff in the ubuntu-window by marking and pressing CTRL-C.

There are two tools that can get the dependencies and compile Agda for you, “cabal” and “stack”. I prefer to use stack:

https://docs.haskellstack.org/en/stable/README/

After installing, stack asked me to append something to my PATH, which I did only for the session:

export PATH=$PATH:/home/USER/.local/bin

Getting the sources and compiling

Git is preinstalled, so you can just get the agda sources with:

git clone https://github.com/agda/agda.git

Go into the agda folder. It will contain a couple of files with names like

stack-8.8.1.yaml

These are configuration files for stack. The numbers indicate the version of ghc (the haskell compiler) that will be used. I take always the newest version (if everything works with it…) and make a copy

cp stack-8.8.1.yaml stack.yaml

– since stack will just use the “stack.yaml” for configuration when run in a folder. Now:

stack setup

will download ghc binaries and install them somewhere below “HOME/.stack/”. Before building, we have to install a dependency (otherwise there will be a linker error with the current ubuntu app):

sudo apt install libtinfo-dev

Then tell stack to build and hope for the best (that took around 5.2GB of RAM and half an hour on my system…):

stack build

On success, it should look like this:
agda_folders

If you are not confident with finding the locations from the last lines again, you should secure the path from the last lines. We will need “agda” and “agda-mode”, which are in the same folder.

Using Agda

Of course, you can use agda from the command line, but it is a lot more fun to use from emacs (or, possibly atom, which I have not checked out). Since the ubuntu app does not come with a window system and on the other hand our freshly built agda cannot be invoked easily from windows programs, I found it most convenient to run emacs in the ubuntu app, but use an x-server in windows.

For the latter, you can install Xming and start it. Then install emacs in the ubuntu app:

sudo apt install emacs

Before starting emacs, we should install the “agda-mode” for emacs. This can be done by

./stack/install/[LONG PATH FROM ABOVE]/bin/agda-mode setup

Now run emacs with the variables “DISPLAY” set to something which connects it to Xming and “PATH” appended by the long thing from above, so emacs can find agda (and agda-mode):

PATH=$PATH:~/agda/.stack-work/[LONG PATH FROM ABOVE]/bin/ DISPLAY=:0 emacs

Then everything should work and you can test the agda-mode, for example with a new file containing the following:

agda-mode-test

CTRL-C, CTRL-L tells agda-mode to check and highlight the contents of the file.  Here is more on using the agda-mode. Have fun!

Sources:

Resources should follow responsibilities

In the german military forces, there is a new idea coming into effect: Give your commanders the ability to spend free expenses (linked article is in german language). Like, if your battailon lacks sunglasses, you don’t have to wait for bureaucracy to procure them for you (and it probably takes longer than the sun is your immediate problem), you can go out and just buy them.

This is not a new idea, and not a bad one. It implements a simple principle: Resources follow responsibilities. If you have goals to reach, decisions to make and people to manage, you need proper resources. And by resources, I don’t only mean money. Some leniency in procedures, maneuvering space (both real and figuratively) and time are resources that can’t be bought with money, but are essential sometimes.

At our company, we installed this principle over a decade ago. The “creativity budget” is a budget of free expenses for each employee to improve their particular working situation. This might mean a new computer mouse, a conference visit or a specific software. You, the employee, are at the frontline of your work and probably knows best what’s needed. Our creativity budget is the means to obtain it, no questions asked.

And this shows the underlying core principle: Responsibilities follow trust. If I trust you to reach the goals, to make the right decisions and to manage your team, it would be inconsequential to not give you the proper responsibilities. And, transitively, to provide you with adequate resources. As it seems, responsibilities are the middle man between trust and resources.

At our company, you don’t need to invest your free expenses for basic work attire. We are software engineers, so “work attire” means a high-class computer (with several monitors, currently our default is three), a powerful notebook, a decent smartphone and all the non-technical stuff that will determine your long-term work output, like a fitting desk and your personal, comfortable work chair.

For me, it was always consequential that great results can only come from the combination of a great developer and great equipment. I cannot understand how it is expected from developers to produce top-notch software on mediocre or even subpar computers and tools. In my opinion, these things strongly relate with each other. Give your developers good equipment and good results will follow. Putting it in a simplistic formula: the ability of the developer multiplied with the power of the equipment makes the quality of the software result.

So, if I trust your ability as a developer, provide you with premium equipment, give you room to maneuver and resources to cover your individual requirements, there should be nothing in the way to hold you back. And that places another responsibility onto your shoulder: You are responsible for your work results. And you deserve all the praise for the better ones. Because without you, the able developer, all the prerequisites listed above would still yield to nothing.

Gradle projects as Debian packages

Gradle is a great tool for setting up and building your Java projects. If you want to deliver them for Ubuntu or other debian-based distributions you should consider building .deb packages. Because of the quite steep learning curve of debian packaging I want to show you a step-by-step guide to get you up to speed.

Prerequisites

You have a project that can be built by gradle using gradle wrapper. In addition you have a debian-based system where you can install and use the packaging utilities used to create the package metadata and the final packages.

To prepare the debian system you have to install some packages:

sudo apt install dh-make debhelper javahelper

Generating packaging infrastructure

First we have to generate all the files necessary to build full fledged debian packages. Fortunately, there is a tool for that called dh_make. To correctly prefill the maintainer name and e-mail address we have to set 2 environment variables. Of course, you could change them later…

export DEBFULLNAME="John Doe"
export DEBEMAIL="john.doe@company.net"
cd $project_root
dh_make --native -p $project_name-$version

Choose “indep binary” (“i”) as type of package because Java is architecture indendepent. This will generate the debian directory containing all the files for creating .deb packages. You can safely ignore all of the files ending with .ex as they are examples features like manpage-generation, additional scripts pre- and post-installation and many other aspects.

We will concentrate on only two files that will allow us to build a nice basic package of our software:

  1. control
  2. rules

Adding metadata for our Java project

In the control file fill all the properties if relevant for your project. They will help your users understand what the package contains and whom to contact in case of problems. You should add the JRE to depends, e.g.:

Depends: openjdk-8-jre, ${misc:Depends}

If you have other dependencies that can be resolved by packages of the distribution add them there, too.

Define the rules for building our Java project

The most important file is the rules makefile which defines how our project is built and what the resulting package contents consist of. For this to work with gradle we use the javahelper dh_make extension and override some targets to tune the results. Key in all this is that the directory debian/$project_name/ contains a directory structure with all our files we want to install on the target machine. In our example we will put everything into the directory /opt/my_project.

#!/usr/bin/make -f
# -*- makefile -*-

# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1

%:
	dh $@ --with javahelper # use the javahelper extension

override_dh_auto_build:
	export GRADLE_USER_HOME="`pwd`/gradle"; \
	export GRADLE_OPTS="-Dorg.gradle.daemon=false -Xmx512m"; \
	./gradlew assemble; \
	./gradlew test

override_dh_auto_install:
	dh_auto_install
# here we can install additional files like an upstart configuration
	export UPSTART_TARGET_DIR=debian/my_project/etc/init/; \
	mkdir -p $${UPSTART_TARGET_DIR}; \
	install -m 644 debian/my_project.conf $${UPSTART_TARGET_DIR};

# additional install target of javahelper
override_jh_installlibs:
	LIB_DIR="debian/my_project/opt/my_project/lib"; \
	mkdir -p $${LIB_DIR}; \
	install lib/*.jar $${LIB_DIR}; \
	install build/libs/*.jar $${LIB_DIR};
	BIN_DIR="debian/my_project/opt/my_project/bin"; \
	mkdir -p $${BIN_DIR}; \
	install build/scripts/my_project_start_script.sh $${BIN_DIR}; \

Most of the above should be self-explanatory. Here some things that cost me some time and I found noteworthy:

  • Newer Gradle version use a lot memory and try to start a daemon which does not help you on your build slaves (if using a continous integration system)
  • The rules file is in GNU make syntax and executes each command separately. So you have to make sure everything is on “one line” if you want to access environment variables for example. This is achieved by \ as continuation character.
  • You have to escape the $ to use shell variables.

Summary

Debian packaging can be daunting at first but using and understanding the tools you can build new packages of your projects in a few minutes. I hope this guide helps you to find a starting point for your gradle-based projects.

Internet in China

If you’re traveling to China you have to be prepared that a lot of sites you are using daily might be blocked due to the Great Firewall. Recently I was there on a business trip as a software developer and here are my notes on what works and what doesn’t, including some tips.

What doesn’t work

Google and its services (Gmail, YouTube) are not available. You can use Bing and Yahoo as search engines. I was using Bing. Bing
recognized that I was using English search queries and offered to switch the user interface to English.

Since all of Google’s domains seem to be blocked, web sites referencing Google API JavaScript files, for example StackOverflow, can take a long time to load before a request timeout kicks in and the rest of the site is displayed. One simple workaround is to disable JavaScript in your browser. This works well for sites that don’t depend too much on JavaScript for their content.

WhatsApp, Facebook, Instagram and Twitter are not available. Since I don’t use them anyway I didn’t miss them. Some news sites occasionally embed Instagram pictures and Twitter posts in their articles, for example announcements by the US president or similar.  You won’t see those either.

What works

Here are some services and websites I was using without problems:

  • Skype is working
  • TeamViewer is working
  • Github is available
  • Wikipedia is available (the non-Chinese language versions)
  • Amazon is working

There are sites where you can check in advance if your favorite websites are accessible. There’s also an overview with the status of high-ranking websites on Wikipedia.

VPN

Apparently using a VPN is not illegal, but access to a lot of VPN services is blocked. If you want to use a VPN app you should download it before entering the country. I personally didn’t feel the need to use a VPN.

Text editing tricks

Multiple cursors

Recently I was in a pair programming session, when I noticed that there were three cursors blinking in the editor window of the IDE. I initially assumed it was a bug in the IDE (which is not that uncommon), but it acutally turned out it was a feature. In IntelliJ based IDEs you can place multiple cursors in the editor window, start typing and the typed text gets inserted at all of these positions. To achieve this press Shift+Alt while clicking the mouse to position the cursor carets.

When I start using a new IDE I usually look up and memorize the shortcuts for refactoring operations like “rename” or “extract method” or other essential operations like “quick fix”.

But of course there are many other neat tricks for advanced text editing in most IDEs and programming editors. Here are some of them, in this case for IntelliJ based IDEs.

Rectangular selection

Rectangular selection

This one comes in handy when you have to select a column of text, for example a common prefix of keys in a properties file. I initially knew this type of selection from Vim, but many other programming editors allow it too. For a rectangular selection in IntelliJ based IDEs press Ctrl+Shift+Alt (Shift+Alt+Cmd on Mac) and drag the mouse pointer.

Multiselection

Similar to the multiple cursors feature mentioned at the beginning of this post, you can also select multiple parts of a text at once and then cut, copy or delete them. To achieve this multi-selection press Shift+Alt while selecting text.

Multiple selction

Extending selection

By pressing Ctrl+W repeatedly within a fragment of code the selection will progressively extend. First the current expression under the cursor is selected, then the surrounding code block, then the code block surrounding this code block, etc.

Extending selection

Conclusion

Take some time and look up some of the more advanced text editing capabilities of your IDE or text editor. Adopt them if you find them helpful and share them with your colleagues, for example in a pair programming session.

Packaging Python projects for Debian/Ubuntu

Deployment of software using built-in software management tools is very convenient and provides a nice user experience (UX) for the users. For debian-based linux distributions like Ubuntu packaging software in .deb-packages is the way to go. So how can we prepare our python projects for packaging as a deb-package? The good news is that python is supported out-of-the-box in the debian package build system.

Alternatively, you can use the distutils-extension stdeb if you do not need complete flexibility in creating the packages.

Basic python deb-package

If you are using setuptools/distutils for your python project debian packaging consists of editing the package metadata and adding --with python to the rules file. For a nice headstart we can generate templates of the debian metadata files using two simple commands (the debhelper package is needed for dh_make:

# create a tarball with the current project sources
python setup.py sdist
# generate the debian package metadata files 
dh_make -p ${project_name}_${version} -f dist/${project_name}-${version}.tar.gz 

You have to edit at least the control-file, the changelog and the rules-file to build the python package. In the rules-file the make-target % is the crucial point and should include the flag to build a python project:

# main packaging script based on dh7 syntax
%:
	dh $@ --with python

After that you can build the package issueing dpkg-buildpackage.

The caveats

The debian packaging system is great in complaining about non-conformant aspects of your package. It demands digital signatures, correct file and directory names including version strings etc. Unfortunately it is not very helpful when you make packaging  mistakes resulting in empty, incomplete or broken packages.

Issues with setup.py

The setup.py build script has to reside on the same level as the debian-directory containing the package metadata. The packaging tools will not tell you if they could not find the setup script. In addition it will always run setup.py using python 2, even if you specified --with python3 in the rules-file.

Packaging for specific python versions

If you want better control over the target python versions for the package you should use Pybuild. You can do this by a little change to the rules-file, e.g. a python3-only build using Pybuild:

# main packaging script based on dh7 syntax
%:
	dh $@ --with python3 --buildsystem=pybuild

For pybuild to work it is crucial to add the needed python interpreter(s) besides the mandatory build dependency dh-python to the Build-Depends of the control-file, for python3-only it could look like this:

Build-Depends: debhelper (>=9), dh-python, python3-all
...
Depends: ${python3:Depends}

Without the dh-python build dependency pybuild will silently do nothing. Getting the build dependencies wrong will create incomplete or broken packages. Take extra care of getting this right!

Conclusion

Debian packaging looks quite intimidating at first because there are so many ways to build a package. Many different tools can ease package creation but also add confusion. Packaging python software is done easily if you know the quirks. The python examples from the Guide for Debian Maintainers are certainly worth a look!

A good name will shine forever

Naming things is supposedly one of the two hard things in Computer Science. Here are some tips on naming for programmers.

Getters

In the Java world property accessors are traditionally prefixed with “get” and “set”, the Java bean convention:

person.getFirstName()

Code becomes more pleasant to read if you omit the “get” prefix:

person.firstName()

Of course, you can do this only if you don’t use a framework that depends on the convention to recognize properties via reflection (like some OR mappers, for example).

What about setters? I rarely write setters anymore. If you design your classes as immutable types you don’t need setters. Even if your class has mutable state you probably want to control this state via methods more specific to the domain of the problem. Also, the more you apply the tell, don’t ask principle the less you will find the need for getters.

Brevity vs. verbosity

There were times when it was common to see mass variable declarations like the following at the beginning of a function:

int i, j, k, l, m, n;
float a, b, c, u, v, x, y, z;

Fortunately, times have changed for the better, and most programmers are aware that descriptive naming is important. However, some programmers do over-compensate. Length of an identifier is not a virtue by itself.

The Objective-C Cocoa framework is famous for overly long method names:

[array objectAtIndex:index]

Parts of Objective-C were inspired by Smalltalk. But in Smalltalk the same method is called at:

[array at:index]

This is a reasonably sufficient name for such a common functionality in programming.

Here’s another example: If the concept of a measurement station is very prevalent in the domain of your project then it’s ok to call instances just station instead of measurementStation if it’s the only kind of station in the domain.

Yes, the IDE does auto-complete long names. However, readability of the code decreases if the reader has to scan the same long-winded names over and over again:

MeasurementStation measurementStation = new MeasurementStation();
Measurement measurement = measurementStation.startMeasurement();

Often you can find names that are more to the point than longer descriptions, e.g. acquire instead of takeOwnershipOf. (source)

Hungarian notation and friends

The famous Hungarian notation is no longer in widespread use. However, there are variations of it that I would recommend against as well for the sake of readability. For example, bookList or bookArray can be simply books. Another variation would be conventions like myField or m_field for member variables. If you need these notations to determine the origin of a variable, then your scopes are probably too big, i.e. your methods, functions or classes are too long. Additionally, IDEs and editors for programmers can highlight these different scopes anyway. Other examples for unnecessary Hungarian-style notation are IFoo for interfaces, EFoo for enums or the infamous FooImpl.

Screaming constants

There is really no need for constants and enum values to constantly SCREAM at you and other readers. This SCREAMING_CASE convention has its origin in C, where constants used to be defined as macros when the const keyword wasn’t introduced yet, and it later found its way into other programming language ecosystems. Names for constants and enum values are not more important than other identifiers and don’t have to be spelled differently. Try it, you will enjoy the newfound silence in your code.

Conclusion

These are some tips to improve readability of code through better names. Some of these tips go against traditional conventions, so you should discuss them with your team before applying them. Consistency within an existing code base can definitely be more important. But if you have the freedom you should definitely give them a try.