catalin-hritcu

module Tree

(* We illustrate the power of our semantic termination check on the
   example of arbitrarily branching trees *)

type tree (a: Type u#a) =
  | Leaf : v:a -> tree a
  | Branch : subtrees:(list u#a (tree a)) -> tree a

let rec list_map (#a:Type) (xs:list a) (f:(x:a{x<<xs} -> 'b)) : list 'b =

catalin-hritcu

TeX log appears below

[verbose]: Creating arXiv submission AutoTeX object
[verbose]: *** Using TeX Live 2016 ***
[verbose]: Calling arXiv submission AutoTeX process
[verbose]: TeX/AutoTeX.pm: admin_timeout = minion
[verbose]: <parametricity.tex> is of type 'TEX'.
[verbose]: <Effects.tex> is of type 'TEX'.
[verbose]: <conclusions.tex> is of type 'unknown'.
[verbose]: <future-work.tex> is of type 'unknown'.

catalin-hritcu

TeX log appears below

[verbose]: Creating arXiv submission AutoTeX object
[verbose]: *** Using TeX Live 2016 ***
[verbose]: Calling arXiv submission AutoTeX process
[verbose]: TeX/AutoTeX.pm: admin_timeout = minion
[verbose]: <robust_diff_traces.tex> is of type 'TEX'.
[verbose]: <instance-more-target-statements.tex> is of type 'TEX'.
[verbose]: <expand-sec-diagram.tex> is of type 'TEX'.
[verbose]: <diagram-prop-pres-comp-security.tex> is of type 'TEX'.

catalin-hritcu

#!/usr/bin/env python
# -*- coding: utf-8 -*-

from zeus import core

def load_file(file_name):
    fd = open(file_name, "r")
    data = core.from_canonical(fd)
    fd.close()
    return data

catalin-hritcu

$ git clone git@github.com:grnet/zeus.git
$ cd zeus
zeus$ cp deploy/config.yaml.example deploy/config.yaml
zeus$ docker build .
zeus$ docker images      # get the IMAGE_ID of the latest created image (mine was 80f4947e565e, but it will be different)
zeus$ docker run -v /home/hritcu/Life/usr/2019-09-02-presedinte-usr:/proofs --shm-size=5120m --entrypoint /bin/bash -it 80f4947e565e
  # where /home/hritcu/Life/usr/2019-09-02-presedinte-usr is where I put Mircea's proof files
  # where --shm-size=5120m is there to prevent: "OSError: [Errno 28] No space left on device"
  # this will log you into the docker image

catalin-hritcu

-*- mode: compilation; default-directory: "~/Projects/fstar/kenji-phd/" -*-
Compilation started at Fri Aug  2 13:23:11

make -k
rm -f main.log
pdflatex -synctex=-1  -interaction nonstopmode main &> /dev/null
make: [Makefile:13: pulp] Error 1 (ignored)
bibtex main | sed -r -e "/Repeated entry/,/I'm skipping/ d"
This is BibTeX, Version 0.99d (TeX Live 2019/Arch Linux)
The top-level auxiliary file: main.aux

catalin-hritcu

[hritcu@killmanjaro doublylinkedlist]$ /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/bin/fstar.exe  --z3cliopt 'timeout=600000' --smtencoding.valid_intro true --smtencoding.valid_elim true --use_hints --use_extracted_interfaces true DoublyLinkedList.fst --debug true --query_stats
Opening file DoublyLinkedList.fst
Reading the parsing data for /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/ulib/FStar.Classical.fsti from its checked file
Reading the parsing data for /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/ulib/FStar.Pervasives.fst from its checked file
Reading the parsing data for /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/ulib/FStar.Pervasives.Native.fst from its checked file
Reading the parsing data for /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/ulib/prims.fst from its checked file
Reading the parsing data for /home/hritcu/Projects/fstar/pub/src/ocaml-output/fstar/ulib/FStar.Classical.fst from its checked file
Reading the parsing data for /home/hritcu/Pro

catalin-hritcu

artagnon   [May 6th at 9:38 AM]
I wish `fstar.exe --ide` implemented the Language Server Protocol; it would be really easy to do editor integration then: https://microsoft.github.io/language-server-protocol/ (edited)

19 replies

artagnon   [2 days ago]
The editor plugin for clangd is as simple as this: https://github.com/llvm-mirror/clang-tools-extra/blob/master/clangd/clients/clangd-vscode/src/extension.ts


catalin   [2 days ago]

catalin-hritcu

catalin   [Mar 27th at 8:22 PM]
Noob question of the day. Can we fix `make -C examples/hello fs`? (It's our simple example of how to extract things to F# and run them.)
https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help/topic/Compiling.20to.20F.23 (edited)
51 replies

nik   [1 month ago]
Not really an answer to your question, but somewhat related

nik   [1 month ago]
I was thinking last night while trying to debug stuff related to a nasty performance problem that the F# build of fstar.exe is really not providing me with that much value.

catalin-hritcu

fsharpc --mlcompatibility --nowarn:0086 -o out/hello.exe ../../ulib/fs/prims.fs ../../ulib/fs/io.fs out/Hello.fs
Microsoft (R) F# Compiler version 10.2.3 for F# 4.5
Copyright (c) Microsoft Corporation. All Rights Reserved.

/home/hritcu/Projects/fstar/pub/ulib/fs/prims.fs(4,21): error FS0039: The namespace 'Compatibility' is not defined.

/home/hritcu/Projects/fstar/pub/ulib/fs/prims.fs(6,19): error FS0039: The namespace 'Compatibility' is not defined.

/home/hritcu/Projects/fstar/pub/ulib/fs/prims.fs(14,21): error FS0039: The type 'Z' is not defined.