EJCP 2014

École Jeunes Chercheurs en Programmation

body

Parallel program calculation in Coq

Programming with Dependent Types (Agda)

install Emacs
install the Haskell platform (http://www.haskell.org/platform/)

install Agda

cabal update
cabal install Agda
agda-mode setup

To set the path from inside emacs, add this to your emacs configuration file

(setenv "PATH" (concat "~/.cabal/bin:"
                       (getenv "PATH")))

Course page

Programming the Diffuse Web (Hop)

Slides (uncompress this file and view it with Chrome)
TD 1 TD 2
Solutions to the exercises number1.js number2.js image.js

Ressources: html5rocks

Downloading the packages

The simplest approach is to use these versions:

Since these links are only live till the end of EJCP, you may want to follow the next instructions to download the packages if you are reading this after June 20.

HOP is available from the Inria ftp repository as a source archive Go to

ftp://ftp-sop.inria.fr/indes/fp/hop

and then select the appropriate archive file, most likely hop-3.0.0-<something> since we want to use JavaScript as our main programming language (hop-2.5 does not support js). You also need to download bigloo (a set of compilers and run-time environments on which HOP is built), from the same ftp server Go to

ftp://ftp-sop.inria.fr/indes/fp/bigloo

and select the recommended bigloo archive (currently a tagged alpha version of bigloo-4.2)

Pre installation suggestions

Please use the version of the software that we recommend. When it is time to change to a newer version, we’ll let you know. Before you install HOP :

Prepare a linux, unix, or OSX environment (Windows users : use linux through virtualbox)
HOP and Bigloo auto configure themselves depending on the environment at the time ./configure is run in the bigloo and HOP build directories. So it is important that you properly install third party libraries before you run ./configure Libuv is required. Sqlite3 is useful.
- Linux users : do not forget to sudo ldconfig after a lib install
- If you add a support lib at a later time please “make clean” then rebuild bigloo and HOP

To Install HOP

Checking your libuv installation
Since hop require bigloo to be built with libuv, you should first make sure bigloo will be compiled with it. To check it, you can run
```
cd bigloo-4.2.a
./configure
```
and make sure that the configuration summary mentions libuv (typically the last item of APIs).

If it does not, you first need to install libuv. On OS X, you can install homebrew then run
```
brew install libuv --devel
```
Otherwise, you can fetch it here, uncompress it, then
```
cd libuv-0.11.25/
./autogen.sh
./configure
```
In the output, make sure you have checking for pkg-config... yes.

You can then install libuv
```
make; sudo make install
```
Installing bigloo
```
cd bigloo-4.2.a; ./configure; make; sudo make install; ldconfig
```
(the last step is not necessary under OS X)

Troubleshooting the bigloo installation :

– Make sure that the build directory is writable (by you, and also by the root user)

– Look at configure.log in the build directory

– Look at /usr/local/lib (default installation path) for bigloo installed libs and /usr/local/bin for executables
Installing HOP
```
cd hop-3.0.0-prexXXX; ./configure; make; sudo make install; ldconfig
```
(the last step is not necessary under OS X)

Troubleshooting : installed libs and executables located in /usr/local. Make sure that your PC firewall does not block incoming http requests from localhost

Change the listening port if it is already used by some other application (note that hop needs to be launched as root to open port 80)

Configure HOP

Launch /usr/local/bin/hop from a terminal

– Default port is 8080 (same as launching hop – p 8080)

Launch a browser on http://localhost:8080/hop

Follow configuration steps as requested (this will create default hoprc.hop and wizard.hop files in ~/.config/hop)

Relaunch hop, direct your browser to the same url and navigate through the built in demos and documentation.

Be aware of potential privacy issues: depending on your configuration parameters, you may expose all your home dir to the world … maybe not a good idea!

Emacs mode

Download this file and add the initialization code at the end of the file to your emacs configuration.

Programming and Proving : Practice with FoCaLiZe

Information about the course, including what to install, is available here.

Computer-aided cryptographic proofs

The first lab session will rely on this web application http://37.139.2.96:7777/tutor/

The second lab session will rely on EasyCrypt. Installation is optional; the installation instructions may be found at https://www.easycrypt.info/trac/