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== 

soonhokong

#!/usr/bin/env bash
sudo add-apt-repository --yes ppa:leanprover/lean
sudo apt-get -qq update
sudo apt-get -qq install lean
 
mkdir ~/workspace/.c9/runners

cat << EOF > ~/workspace/.c9/runners/Lean.run
// Create a custom Cloud9 runner - similar to the Sublime build system
// For more information see https://docs.c9.io/custom_runners.html

soonhokong

#!/usr/bin/env bash
#
# Usage: ./exit_code_wrapper.sh /path/to/dReal /path/to/smt2 option_to_dReal1 option_to_dReal2 option_to_dReal3 ...
#
# Return:
#
#     51     if smt2 is SAT
#     52     if smt2 is UNSAT
#      1     if there is any error
#

soonhokong

Example

This is a slightly modified example based on capdDynSys4/examples/encloseTrajectory/encloseTrajectoryBetweenTimeSteps.cpp file. The main difference is the ODE that it computes the enclosed trajectory: "par:k_0;var:t_0, v_0;fun:1.0, (k_0*t_0)" and the time of integration, 17.

Modified lines are commented with // <----- MODIFIED.

Code

soonhokong

Code from CAPD Author

#include <iostream>
#include "capd/capdlib.h"
using namespace std;
using namespace capd;

int main(){
  cout.precision(17);

soonhokong

#! /usr/bin/env bash

# Author: Damien Cassou
#
# This is the script I use to build Emacs packages for Ubuntu. These
# packages are uploaded to
# https://launchpad.net/~cassou/+archive/emacs/. Each package is
# either build from a Debian package or from
# http://emacs.naquadah.org/.

soonhokong

#!/bin/sh

# This script will setup Evm (Emacs Version Manager) and Cask on
# Travis to use for Emacs Lisp testing.
#
# In .travis.yml, add this:
#
#  - curl -fsSkL https://gist.github.com/rejeep/7736123/raw > travis.sh && source ./travis.sh
#
# Emacs 24.3 is installed in the above script because Cask requires