魂斗罗游戏java源码-notes:博士日记

魂斗罗游戏java源码13.03.2018 字节码和本机可执行文件中的数组性能 由于leanCoP/nanoCoP 在HOL Light 中的证明搜索性能相当令人失望，Cezary 表示OCaml 字节码中数组速度慢可能是罪魁祸首。 为此，我创建了一个小测试程序来测试数组访问速度： let _ = let a = Array. make 100000 0 in let s = ref 0 in for x = 0 to 100000 do for i = 0 to 99999 do s := a.(i) done ; done ; Format. printf " done \n " 结果如下所示。 这些数字表明，本机数组的执行速度比字节码数组快 35 倍（！），禁用边界检查再次使速度加倍。 执行 时间 字节码 3分32秒 本国的 6s 原生（不安全） 3s 不安全编译是通过以下方式实现的： ocamlbuild -ocamlopt "ocamlopt -unsafe -inline 100" test.native 07.02.2018 为所有 HOL Light 战术创建已解决的文