Chris doublec
doublec
/ fact_z3_threaded.dats
Created
October 6, 2019 12:01
ATS proofs about factorial using threaded Z3 proofs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ATS factorial proof examples, based on F* tutorial examples at: | |
| // https://www.fstar-lang.org/tutorial/ | |
| // | |
| // patsopt -tc --constraint-export -d fact_z3_threaded.dats |patsolve_z3 -i | |
| // | |
| #include "share/atspre_define.hats" | |
| #include "share/atspre_staload.hats" | |
| stacst fact: int -> int |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ATS factorial proof examples, based on F* tutorial examples at: | |
| // https://www.fstar-lang.org/tutorial/ | |
| // | |
| // patsopt -tc --constraint-export -d fact_prop.dats |patsolve_z3 -i | |
| // | |
| #include "share/atspre_define.hats" | |
| #include "share/atspre_staload.hats" | |
| dataprop FACT (int, int) = | |
| | FACTzero (0, 1) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Build musl libc | |
| $ git clone git://git.musl-libc.org/musl | |
| $ cd musl | |
| $ ./configure | |
| $ make | |
| $ sudo make install | |
| $ export PATH=$PATH:/usr/local/musl/bin/ | |
| # build libz for musl | |
| $ wget https://zlib.net/zlib-1.2.11.tar.gz |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Build musl libc | |
| $ git clone git://git.musl-libc.org/musl | |
| $ cd musl | |
| $ ./configure | |
| $ make | |
| $ sudo make install | |
| $ export PATH=$PATH:/usr/local/musl/bin/ | |
| # build libz for musl | |
| $ wget https://zlib.net/zlib-1.2.11.tar.gz |
doublec
/ gist:d4598ce955172306fef733f6e860b97f
Created
February 16, 2018 01:07
Building terralang from source
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Building Terralang (http://terralang.org/) from source | |
| $ export BUILD_ROOT=`pwd` | |
| # Build LLVM 3.9 | |
| $ git clone https://github.com/llvm-mirror/llvm --branch release_39 | |
| $ cd $(BUILD_ROOT)/llvm/tools | |
| $ git clone https://github.com/llvm-mirror/clang --branch release_39 | |
| $ cd $(BUILD_ROOT)/llvm | |
| $ mkdir build |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* | |
| $ patscc -o gadt gadt.dats | |
| $ ./gadt | |
| res1=true and res2=8 | |
| *) | |
| #include "share/atspre_define.hats" | |
| #include "share/atspre_staload.hats" | |
| datatype Expr (t@ype) = | |
| | I(int) of int |
doublec
/ gist:c2e3c0ab05d622de4de9fa389b0f9d78
Created
August 28, 2017 06:30
Static binaries in ATS using musl-libc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ cat hello.dats | |
| implement main0() = print!("Hello World\n") | |
| $ patscc -atsccomp "/usr/local/musl/bin/musl-gcc" -static -I$PATSHOME/ccomp/runtime -I$PATSHOME hello.dats | |
| $ ./a.out | |
| Hello World | |
| $ ldd ./a.out | |
| not a dynamic executable | |
| $ strip ./a.out | |
| $ ls -l ./a.out | |
| -rwxr-xr-x 1 user user 18080 Aug 28 18:29 a.out |
doublec
/ gist:e34db117d46b61a39d768d526c00257e
Created
December 4, 2016 20:38
Reverse Factorial using constraints in Mozart/Oz
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| proc {Fact ?N ?F} | |
| proc {Fact1 ?N ?F} | |
| choice | |
| N = 0 | |
| F = 1 | |
| [] | |
| N1 F1 | |
| in | |
| N1::0#FD.sup | |
| F1::0#FD.sup |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| actor Main | |
| new create(env:Env) => | |
| let fac = lambda (n:U32): U32 => if n == 0 then 1 else n * this(n - 1) end end | |
| env.out.print("fac 5 = " + fac(5).string()) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ sudo apt-get install gcc-multilib g++-multilib libx11-dev:i386 libXext-dev:i386 libncurses5-dev:i386 | |
| $ git clone https://github.com/doublec/self | |
| $ cd self | |
| $ make -f Makefile.linux | |
| $ cd objects | |
| $ ../vm/Self | |
| Self Virtual Machine Version 4.1.13, Fri 02 Oct 15 09:48:48 Linux i3864.4.alpha2-437-g43ebab6 | |
| Copyright 1989-2003: The Self Group (type _Credits for credits) | |
| for I386: LogVMMessages = true |
NewerOlder