Skip to content
This repository has been archived by the owner on Jun 17, 2024. It is now read-only.

Development environment

Jump to bottom
Jonathan Protzenko edited this page Jul 25, 2016 · 5 revisions

This pages lists one known working setup that the author believes to be pretty much what everyone in the team uses. Hit me (protz) up or edit this page if you have questions / improvements. Some of these points about Git & Windows also apply to F*.

Table of contents

Git, Cygwin, Windows and happiness

Most of us use Cygwin, and hardly ever open a cmd prompt. The git we use is the git package from Cygwin. We use this: https://github.com/protz/ocaml-installer/wiki to get a working Cygwin setup and a working OCaml setup in there. Here are some classic problems you may encounter when using Git on Windows and/or Cygwin after that.

Line endings

Windows uses CRLF. Linux/OSX use LF. Most Windows editors will silently "convert" Unix-style line endings into Windows-style line endings (source: https://git-scm.com/book/en/v2/Customizing-Git-Git-Configuration#Formatting-and-Whitespace). There are two philosophical currents that go about solving this problem:

  • convert files upon checkout to have "native" line-endings, i.e. git.autocrlf = true; let your editor happily insert CRLF everywhere; let git silently convert to LF when committing;
  • don't ask Git to be smart, i.e. git.autocrlf = false; acknowledge the fact that someone, eventually, will attempt to commit a botched file with CRLF in it; use .gitattributes to avoid that problem.

miTLS and F* use the latter. I use a Cygwin editor that never changes line-endings (vim) but some collaborators may use something else; the .gitattributes file prevents them from messing up. If you get:

The file will have its original line endings in your working directory. warning: LF will be replaced by CRLF in Foo.fst

then you edited Foo.fst with an editor that thought it was a good idea to replace all line endings in your file.

Pro tips:

  • git merge and git rebase take a -Xignore-space-change option that can be incredibly handy, especially in the scenario where someone on master rage-removed all the trailing whitespace, and you're trying to merge master into your branch.
  • Cygwin's bash is very unhappy with CRLF; if you add a shell script in miTLS, add it to .gitattributes

File permissions

In the Cygwin git scenario, I've never had any issues with file permissions. But there have been numerous instances of the dreaded "mode conflict" reported in the wild.

diff --git a/foo b/foo
old mode 100644
new mode 100755

Symptoms are the snippet above showing up in your git diff. (And you can't git revert or git checkout these changes away.) git config core.filemode false seems to fix it. Pro tip: you may want to make this git config --global core.filemode false.

Cygwin is slow as hell

Symptoms:

  • any command takes ages to complete
  • if you do a strace of your process, you realize it's searching through the entire Microsoft LDAP address book
  • you can't run a Cygwin program unless you have enabled DirectAccess on your laptop.

Solution: pick solution 2 from https://gist.github.com/k-takata/9b8d143f0f3fef5abdab

Submodule hell

You need to merge but there's a disagreement as to which revision the .fstar submodule should have. You can't git add the submodule. Here's some troubleshooting:

  • cd .fstar && git status should return something clean; if it doesn't, then you need to git reset --hard HEAD in .fstar, but that's strange, because editing the submodule is not recommended; you may be hitting the file permissions bug above, in which case you need to run git config core.filemode false in BOTH mitls-fstar and mitls-fstar/.fstar (or use --global)
  • git add .fstar should, in theory, solve the issue
  • git mergetool will ask you interactively what to do; this may turn in handy.

Some tips and tricks

Here's what I have in my ~/.gitconfig. Please note:

  • autocrlf is false
  • I have no eol setting, meaning that git does not attempt anything smart when checkout out text files.
[user]
  name = Jonathan Protzenko
  email = [email protected]

[color]
  ui = true

[core]
  excludesfile = ~/.gitignore
  pager = less -+$LESS -RSX
  quotepath = false
  autocrlf = false

[push]
  default = current

[advice]
  detachedHead = false

[help]
  autocorrect = 1

General working tips

  • We never edit anything in the .fstar submodule; it will cause git to report a dirty state for the submodule when doing git status in the mitls-fstar directory. This is undesirable.
  • If you need to try out mitls-fstar against some changes you made in F*, then please use your own checkout of F* in some other directory, then FSTAR_HOME=../fstar make -C src/tls tls-gen.
  • There is no policy for line-endings, mostly because I don't know how to enforce the "no trailing-whitespace" policy in Visual Studio and Emacs.

Branching and merging

We expect that the version on master will always, at least, pass tls-gen.

Editor

Mostly, Emacs with the customizations described in https://github.com/mitls/mitls-fstar#configuring-emacs-mode; I recommend using the Cygwin package for Emacs; emacs-w32 is a native Windows program packaged within Cygwin; emacs-x11 uses Cygwin's X11 graphical stack. I use the latter, people have been happy with the former.

Clone this wiki locally