如何看待微軟研究院的LEAN項目沒有使用微軟出品的編譯器?

01-07

Lean Theorem Prover.
項目主頁: Lean
項目地址: leanprover/lean · GitHub

Requirements

C++11 compatible compiler: g++ (version &>= 4.8.1), or clang++ (version &>= 3.3)

CMake

GMP (GNU multiprecision library)

MPFR (GNU MPFR Library)

Lua 5.2 or 5.1, or LuaJIT 2.0

(optional) gperftools

(optional) Boost (version &>= 1.54), we can
build Lean using boost::thread instead of std::thread. When using
Boost, Lean can modify the thread stack size.

MS又不是google或apple，發paper的話本來就是你想用啥都可以。

另外，它依賴於GMP和MPFR，除非自己搞一套替用的，不然就得老老實實g++。一個研究原型沒有任何理由需要把依賴庫都自己搞一遍。那一天要放到產品了再說。研究院很多人的coding不咋地的，你要讓他們替換他們都不一定會做。

MSR嘛。搜「microsoft research java」還能搜出一堆MSR做的Java的研究。

為啥不用C#呢？沒關係高興就好…

似乎聞到了一絲意識形態的鐵鏽味。

IDE只是為編程者服務的工具而已，選擇不同的IDE對於執行效率並沒有什麼決定性影響。

「你開心就好。」

我也很好奇為何他們不一開始就用vs來開發? 不就沒這麼多問題了? 而且vs還是最好用的ide, 開發起來不知道比在linux下開發高多少.

何況那些研究院的人經歷的多了, 操作系統下哪個開發環境沒用過? 難道不知道vs跑得快?

師夷長技以制夷

微軟說：其實我們一開始是拒絕閉源的。

ms love linux

ms研究院的本質上是研究者，而G與Apple的，大多是工程師。