Feature/vm dynload

.appveyor.yml

@@ -1,7 +1,13 @@
 image: Visual Studio 2017
-
+skip_branch_with_pr: true
 environment:
   MSYSTEM: MINGW64  # use MSYS2 shell
+  CYG_ROOT: C:/cygwin
+  CYG_CACHE: C:/cygwin/var/cache/setup
+  CYG_MIRROR: http://mirrors.kernel.org/sourceware/cygwin/
+  VSVER: 15
+  LIBFFI_V: 3.2
+  dlfcn-win32_DIR: C:\projects\vcpkg\installed\x86-windows
   matrix:
   - CFG: MINGW64
     UPLOAD: ON
@@ -13,12 +19,44 @@ install:
   # upgrade git for vcpkg: https://github.com/appveyor/ci/issues/2097
   - if %CFG% == MSVC (choco upgrade git -y & vcpkg install mpir:x64-windows)
 
+  - cd ..
+  - git clone https://github.com/Microsoft/vcpkg
+  - cd vcpkg
+  - .\bootstrap-vcpkg.bat
+  - vcpkg.exe install dlfcn-win32
+  - ls C:\projects\vcpkg\downloads
+  - ls C:\projects\vcpkg\installed\x86-windows
+  - ls C:\projects\vcpkg\installed\vcpkg
+  - ls C:\projects\vcpkg\installed
+
+  - ls C:\projects\vcpkg\installed\*  || true
+  - ls C:\projects\vcpkg\downloads\tools || true
+  - ls C:\projects\vcpkg\downloads\*\* || true
+  # - ls C:\projects\vcpkg\downloads\*\*\*
+  - ls %HOME%
+  - ls %HOME%\installed || true
+  - ls %HOME%\packages || true
+  - ls %HOME%\ports || true
+  - cd %APPVEYOR_BUILD_FOLDER%
+
+  - 'nuget install libffi'
+  # - pwd
+  # - ls
+  # - ls libffi.3.2.1.1/build/native
+  # - ls libffi.3.2.1.1/build/native/*
+  # - ls libffi.3.2.1.1/build/native/*/*/
+  # - ls libffi.3.2.1.1/build/native/*/*/*
+
 build_script:
+  - git submodule update --init --recursive
   - call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Community\VC\Auxiliary\Build\vcvars64.bat"
   - cd %APPVEYOR_BUILD_FOLDER% && mkdir build && cd build
+  - ls c:/projects/lean/libffi.3.2.1.1/build/native/include
   # disable slow LTO
   - if %CFG% == MSVC (cmake ../src
       -DCMAKE_BUILD_TYPE=Release
+      -DFFI_INCLUDE_DIR=c:/projects/lean/libffi.3.2.1.1/build/native/include
+      '-DFFI_LIBRARY_DIR=%APPVEYOR_BUILD_FOLDER%\libffi.3.2.1.1\build\native\lib'
       -DCMAKE_TOOLCHAIN_FILE=c:/tools/vcpkg/scripts/buildsystems/vcpkg.cmake
       -DLEAN_EXTRA_CXX_FLAGS=/GL-
       -DLEAN_EXTRA_LINKER_FLAGS_MSVC=/LTCG:OFF

.gitignore

@@ -22,3 +22,5 @@ settings.json
 /library/init/version.lean
 CMakeSettings.json
 CppProperties.json
+/build
+/_cache/

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "thirdparty/dlfcn-win32"]
+	path = thirdparty/dlfcn-win32
+	url = https://github.com/dlfcn-win32/dlfcn-win32

.travis.yml

@@ -1,7 +1,13 @@
 language: cpp
 sudo: true
-cache: apt
+cache:
+  apt: true
+  ccache: true
 dist: trusty
+branches:
+  only:
+    - master
+    - feature/vm-dynload
 group: deprecated-2017Q3
 addons:
   apt:
@@ -30,6 +36,7 @@ matrix:
        FIRST=1
 
    - os: linux
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=clang++-3.4
        CMAKE_BUILD_TYPE=Release
@@ -44,20 +51,23 @@ matrix:
            - *default_packages
            - g++-6
            - gcc-6
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++-6
        CMAKE_BUILD_TYPE=Release
        TCMALLOC=ON
 
    - os: linux
      addons: *gcc6_addons
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++-6
        CMAKE_BUILD_TYPE=Release
        TESTCOV=ON
 
    - os: linux
      addons: *gcc6_addons
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++-6
        CMAKE_BUILD_TYPE=Release
@@ -70,20 +80,23 @@ matrix:
          packages:
            - *default_packages
            - z3
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++-4.9
        CMAKE_BUILD_TYPE=Release
        TEST=OFF
        TEST_LEANPKG_REGISTRY=ON
 
    - os: linux
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=clang++-3.4
        CMAKE_BUILD_TYPE=Debug
        TCMALLOC=ON
 
    - os: linux
      dist: precise
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++-4.9
        CMAKE_BUILD_TYPE=Debug
@@ -96,6 +109,7 @@ matrix:
        TEST_LEANPKG_REGISTRY=ON
 
    - os: osx
+     if: type != cron
      env:
        CMAKE_CXX_COMPILER=g++
        CMAKE_BUILD_TYPE=Debug
@@ -106,14 +120,22 @@ before_install:
       brew update &&
       (brew install gcc || brew link --overwrite gcc) &&
       brew install gmp &&
+      brew install ccache &&
       # workaround for https://github.com/travis-ci/travis-ci/issues/6307
       command curl -sSL https://rvm.io/mpapis.asc | gpg --import -
       command curl -sSL https://rvm.io/pkuczynski.asc | gpg --import -
       rvm get head || true
     fi
 
+install:
+  - export CXX_FAMILY=`echo $CMAKE_CXX_COMPILER | sed -n "s/\([^\+]*++\).*/\1/p"`
+     # CXX_FAMILY is either `clang++` or `g++`
+  - mkdir -p ~/bin/
+  - chmod +x script/ccache-$CXX_FAMILY
+  - cp script/ccache-$CXX_FAMILY ~/bin/
+  - export PATH="~/bin/:$PATH"
+
 script:
-  - set -e
   - mkdir -p build
   - cd build
   - if [[ $TESTCOV != ON ]]; then TESTCOV=OFF; fi
@@ -130,7 +152,7 @@ script:
       . ../script/setup_nightly.sh
     fi
   - cmake -DCMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE
-          -DCMAKE_CXX_COMPILER=$CMAKE_CXX_COMPILER
+          -DCMAKE_CXX_COMPILER=ccache-$CXX_FAMILY
           -DTESTCOV=$TESTCOV
           -DTCMALLOC=$TCMALLOC
           -DMULTI_THREAD=$MULTI_THREAD

doc/library/vm.md

@@ -0,0 +1,39 @@
+# Lean's Virtual Machine
+
+## Overview
+
+In simple terms Lean's VM is a single-threaded command-based
+interpreter. As it processes a file it adds the commands it
+encounters to a global environment.
+
+The environment is, in simple terms, a map of names to pairs of
+types and values. The type and value are both expressions.
+
+Unless we are evaluating proofs we evaluate expressions in the
+environment using the VM. Every expression in a command is compiled
+to a form of byte code that can be executed by the VM.
+
+## TODO Architecture
+
+## TODO Memory
+
+## Foreign Function Interface
+
+Lean depends on `libffi` for it's foreign function interface on top of
+`dlopen`.
+
+The VM environment has two functions we use to load pointers to
+foreign objects opened with `dlopen`:
+
+1. `environment_load_foreign_object` which uses `vm_dynload` to call
+   `dlopen` and construct a `vm_foreign_object` instance. The instance
+   is added to a special map in the environment declarations.
+
+2. `environment_bind_foreign_symbol` which uses `libffi` to create a
+   `ff_cif` object from the Lean function definition. The `lib_cif`
+   gets stored in the declaration with the function.
+
+When the environment evaluates an expression that calls a function
+from a foreign object it gets the `ffi_cif` for that function,
+initializes the argument values on the stack, and calls the `libffi`
+interface with the handle to the foreign library and the `ffi_cif`.

library/init/data/int/basic.lean

@@ -103,7 +103,7 @@ protected lemma coe_nat_zero : ↑(0 : ℕ) = (0 : ℤ) := rfl
 protected lemma coe_nat_one : ↑(1 : ℕ) = (1 : ℤ) := rfl
 protected lemma coe_nat_succ (n : ℕ) : (↑(succ n) : ℤ) = ↑n + 1 := rfl
 
-protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl
+protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (↑(m + n) : ℤ) := rfl
 protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl
 protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl
 
@@ -265,7 +265,7 @@ protected def div : ℤ → ℤ → ℤ
 | -[1+ m] -[1+ n] := of_nat (succ (m / succ n))
 
 protected def mod : ℤ → ℤ → ℤ
-| (m : ℕ) n := (m % nat_abs n : ℕ)
+| (of_nat m) n := of_nat (m % nat_abs n)
 | -[1+ m] n := sub_nat_nat (nat_abs n) (succ (m % nat_abs n))
 
 -- F-rounding: This pair satisfies fdiv x y = floor (x / y)
@@ -304,6 +304,12 @@ instance : has_mod ℤ := ⟨int.mod⟩
 
 def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n)
 
+/- div / mod -/
+
+protected lemma coe_nat_div_out (m n : ℕ) : ↑m / ↑n = (↑(m / n) : ℤ) := rfl
+
+protected lemma coe_nat_mod_out (m n : ℕ) : ↑m % ↑n = (↑(m % n) : ℤ) := rfl
+
 /-
    int is a ring
 -/

library/init/data/int/order.lean

@@ -304,4 +304,36 @@ eq_of_mul_eq_mul_right Hpos (by rw [one_mul, H])
 theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
 eq_of_mul_eq_mul_left Hpos (by rw [mul_one, H])
 
+lemma mod_lt {p q : ℤ} (h : 0 < q) : p % q < q :=
+begin
+  cases q; [ skip, cases h ],
+  have h₀ := lt_of_coe_nat_lt_coe_nat h,
+  cases p; dsimp [(%),int.mod,sub_nat_nat],
+  { apply coe_nat_lt_coe_nat_of_lt, apply nat.mod_lt _ h₀ },
+  cases h' : (nat.succ (nat.mod p q) - q);
+    dsimp [sub_nat_nat._match_1],
+  { apply coe_nat_lt_coe_nat_of_lt,
+    apply nat.sub_lt h₀ (nat.zero_lt_succ _), },
+  transitivity (0 : ℤ), apply neg_succ_lt_zero,
+  exact h,
+end
+
+lemma nonneg_mod {p q : ℤ} (h : q ≠ 0) : 0 ≤ p % q :=
+begin
+  cases p; dsimp [(%),int.mod,sub_nat_nat],
+  apply of_nat_nonneg,
+  cases h₀ : (nat.succ (nat.mod p (nat_abs q)) - nat_abs q);
+    dsimp [sub_nat_nat._match_1,has_neg.neg],
+  { apply of_nat_nonneg },
+  suffices h₁ : nat.succ (nat.mod p (nat_abs q)) - nat_abs q = 0,
+  { rw h₁ at h₀, cases h₀ },
+  apply nat.sub_eq_zero_of_le,
+  apply nat.mod_lt, apply nat.pos_of_ne_zero,
+  intro h', apply h,
+  cases q,
+  { dsimp [nat_abs] at h',
+    rw h', refl },
+  { cases h' }
+end
+
 end int

library/init/meta/environment.lean

@@ -74,6 +74,11 @@ match env.get d with
 | exceptional.success _      := tt
 | exceptional.exception ._ _ := ff
 end
+
+meta constant add_defn_eqns (env : environment) (opt : options)
+  (lp_params : list name) (params : list expr) (sig : expr)
+  (eqns : list (list (expr ff) × expr)) (is_meta : bool) : exceptional environment
+
 /-- Register the given name as a namespace, making it available to the `open` command -/
 meta constant add_namespace   : environment → name → environment
 /-- Return tt iff the given name is a namespace -/
@@ -153,6 +158,10 @@ meta constant structure_fields : environment → name → option (list name)
 meta constant get_class_attribute_symbols : environment → name → name_set
 /-- The fingerprint of the environment is a hash formed from all of the declarations in the environment. -/
 meta constant fingerprint : environment → nat
+
+meta constant load_foreign_object (env : environment) (n : name) (file_name : string) : environment
+
+
 open expr
 
 meta constant unfold_untrusted_macros : environment → expr → expr