Skip to content

Instantly share code, notes, and snippets.

Soonho Kong soonhokong

View GitHub Profile
View Vim_EditorConfig.md

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/
View loop_vectorize.md

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
soonhokong / leandeps.py
Created Dec 17, 2015
Python3-compatible leandeps.py
View leandeps.py
#!/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
View test.tex
\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
soonhokong / powertrain.drh
Created Dec 7, 2015
Toyota Powertrain Control Benchmark
View powertrain.drh
// 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
soonhokong / ag_bench.sh
Created Oct 22, 2015 — forked from ggreer/ag_bench.sh
My ag benchmark script
View ag_bench.sh
#!/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
View lean_virtual_memory_exhausted.txt
[ 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
View README.md

Ubuntu

OSX

cmake -DCMAKE_CXX_COMPILER=ccache-clang++ \
      -DCMAKE_C_COMPILER=ccache-clang \
@soonhokong
soonhokong / time_step_control.md
Last active Aug 29, 2015
CAPD time step control
View time_step_control.md

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

image1

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.

image2

  1. CAPD4 gives a very good approximation [0.999, 1.0] when we integrate the function from x = -10 to x = 10.
@soonhokong
soonhokong / valgrind trace for segfault
Created Apr 23, 2015
valgrind trace for segfault
View valgrind trace for segfault
==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==
You can’t perform that action at this time.