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.
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. Using CAPD, let's compute for the range X = [-10, 10] whose prob must be less than 1.0.
| #!/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 | |
| # |
| #!/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 |
I recently found a nice emacs-mode, [irony-mode], which can be used with [company-mode], [flycheck-mode], and [eldoc-mode]. It works nicely with CMake-based projects. The document contains a list of instructions for setting things up. I assume that you're using a fresh-installed Ubuntu-12.04.5 (64-bit). It uses [Lean theorem prover][lean] as an example project.
A curated list by Eric Elliott and friends. Suggest links in the gist comments.
Help us turn this into a proper website!
This is a very exclusive collection of only must-have JavaScript links. I'm only listing my favorite links. Nothing else makes the cut. Feel free to suggest links if you think they're good enough to make this list. The really curious should feel free to browse the comments to find other links. I can't guarantee the quality of links in the comments.
| ==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== |
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.
[0.999, 1.0] when we integrate the function from x = -10 to x = 10.
| [ 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 |