soonhokong

Vim + EditorConfig Setup

mkdir -p ~/tmp
cd ~/tmp
wget https://github.com/editorconfig/editorconfig-vim/archive/master.zip
unzip master.zip
mv editorconfig-vim-master/{autoload,doc,plugin} ~/.vim/

soonhokong

Clang Version

Debian clang version 3.3-debian16precise1 (branches/release_33) (based on LLVM 3.3)
Target: x86_64-pc-linux-gnu
Thread model: posix

Code (test.cpp)

soonhokong

#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# Copyright (c) 2015 Microsoft Corporation. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
#
# Authors: Soonho Kong, Leonardo de Moura, Ulrik Buchholtz

# Python 2/3 compatibility
from __future__ import print_function

soonhokong

\documentclass{article}
\usepackage{unixode}    % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/unixode.sty
\usepackage{minted}     % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/minted.sty
% Specify local pygments directory. Do the following in your working directory (where test.tex is located)
% hg clone https://bitbucket.org/leanprover/pygments-main && cd pygments-main && python setup.py build & cd ..
\renewcommand{\MintedPygmentize}{./pygments-main/pygmentize}
\setminted{encoding=utf-8}
\usepackage{fontspec}
\setmainfont{FreeSerif}
\setmonofont{FreeMono}

soonhokong

// Toyota Powertrain Control Verification Benchmark:
// This is based on the following paper:
//
// Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and
// Ken Butts. 2014. Powertrain control verification benchmark. In
// Proceedings of the 17th international conference on Hybrid systems:
// computation and control (HSCC '14). ACM, New York, NY, USA,
// 253-262. DOI=http://dx.doi.org/10.1145/2562059.2562140
//
// Originally written by Kyungmin Bae (kbae@cs.cmu.edu)

soonhokong

#!/bin/bash

function benchmark_rev() {
    REV=$1
    git clean -f &> /dev/null
    git checkout $REV &> /dev/null
    git clean -f &> /dev/null
    if [ $? -ne 0 ]; then
        echo "Checkout of $REV failed!"
        exit 1

soonhokong

[ 51%] [ 51%] [ 51%] [ 51%] cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/contradiction_tactic.cpp.o -c /root/lean/src/library/tactic/contradiction_tactic.cpp
Building CXX object kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o
cd /root/lean/build/kernel && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/kernel.dir/equiv_manager.cpp.o -c /root/lean/src/kernel/equiv_manager.cpp
/usr/bin/cmake -E cmake_progress_repo

soonhokong

Ubuntu

OSX

cmake -DCMAKE_CXX_COMPILER=ccache-clang++ \
 -DCMAKE_C_COMPILER=ccache-clang \

soonhokong

We want to integrate the probability density function for normal distribution:

To simplify the problem, let's pick mean = 0.0, standard deviation = 1.0. In theory, integration of this fuction from x = -oo to x = oo should give P = 1.0.

1. CAPD4 gives a very good approximation [0.999, 1.0] when we integrate the function from x = -10 to x = 10.

soonhokong

==22321== Memcheck, a memory error detector
==22321== Copyright (C) 2002-2012, and GNU GPL'd, by Julian Seward et al.
==22321== Using Valgrind-3.8.1 and LibVEX; rerun with -h for copyright info
==22321== Command: /usr0/home/soonhok/work/lean/bin/lean /usr0/home/soonhok/work/lean/hott/init/datatypes.hlean
==22321== 
==22321== Syscall param set_robust_list(head) points to uninitialised byte(s)
==22321==    at 0x82F8B1: __pthread_initialize_minimal (nptl-init.c:359)
==22321==    by 0x8340B0: (below main) (in /usr0/home/soonhok/work/lean/bin/lean)
==22321==  Address 0x4001630 is not stack'd, malloc'd or (recently) free'd
==22321==