daily pastebin goal
43%
SHARE
TWEET

Untitled

a guest Oct 19th, 2018 72 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. pgiarrusso@SilenceOfTheLambdas:~/git/Coq/needle/knot-esop-2017-case-study/casestudy/needle$ make -k
  2. /Library/Developer/CommandLineTools/usr/bin/make -C fexistsprod
  3. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  4. COQC FExistsProd.v
  5. File "./FExistsProd.v", line 2310, characters 0-1107:
  6. Warning: Not a fully mutually defined fixpoint
  7. (PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
  8. Well-foundedness check may fail unexpectedly.
  9.  [non-full-mutual,fixpoints]
  10. File "./FExistsProd.v", line 2322, characters 0-2664:
  11. Warning: Not a fully mutually defined fixpoint
  12. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  13. Well-foundedness check may fail unexpectedly.
  14.  [non-full-mutual,fixpoints]
  15. COQC DeclarationEvaluation.v
  16. COQC MetaTheory.v
  17. /Library/Developer/CommandLineTools/usr/bin/make -C lomega
  18. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  19. COQC LambdaOmega.v
  20. File "./LambdaOmega.v", line 2043, characters 0-2410:
  21. Warning: Not a fully mutually defined fixpoint
  22. (e.g., TRed_wf_1 and TRed_wf_0 are not mutually dependent).
  23. Well-foundedness check may fail unexpectedly.
  24.  [non-full-mutual,fixpoints]
  25. File "./LambdaOmega.v", line 2070, characters 0-1157:
  26. Warning: Not a fully mutually defined fixpoint
  27. (Kinding_wf_1 and Kinding_wf_0 are not mutually dependent).
  28. Well-foundedness check may fail unexpectedly.
  29.  [non-full-mutual,fixpoints]
  30. File "./LambdaOmega.v", line 2086, characters 0-1056:
  31. Warning: Not a fully mutually defined fixpoint
  32. (e.g., TRedStar_wf_1 and TRedStar_wf_0 are not mutually
  33. dependent).
  34. Well-foundedness check may fail unexpectedly.
  35.  [non-full-mutual,fixpoints]
  36. File "./LambdaOmega.v", line 2104, characters 0-2740:
  37. Warning: Not a fully mutually defined fixpoint
  38. (TyEq_wf_2 and TyEq_wf_0 are not mutually dependent).
  39. Well-foundedness check may fail unexpectedly.
  40.  [non-full-mutual,fixpoints]
  41. File "./LambdaOmega.v", line 2137, characters 0-1148:
  42. Warning: Not a fully mutually defined fixpoint
  43. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  44. Well-foundedness check may fail unexpectedly.
  45.  [non-full-mutual,fixpoints]
  46. File "./LambdaOmega.v", line 2181, characters 0-61:
  47. Warning: obligation_Env_reg_TRed is declared as a local axiom
  48. [local-declaration,scope]
  49. COQC DeclarationEvaluation.v
  50. COQC MetaTheory.v
  51. File "./MetaTheory.v", line 278, characters 4-56:
  52. Error: Unable to find an instance for the variables S1, S2.
  53. make[2]: *** [MetaTheory.vo] Error 1
  54. make[2]: Target `all' not remade because of errors.
  55. make[1]: *** [coq] Error 2
  56. make: *** [lomega] Error 2
  57. /Library/Developer/CommandLineTools/usr/bin/make -C fomega
  58. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  59. COQC FOmega.v
  60. File "./FOmega.v", line 2227, characters 0-2708:
  61. Warning: Not a fully mutually defined fixpoint
  62. (e.g., TRed_wf_1 and TRed_wf_0 are not mutually dependent).
  63. Well-foundedness check may fail unexpectedly.
  64.  [non-full-mutual,fixpoints]
  65. File "./FOmega.v", line 2257, characters 0-1327:
  66. Warning: Not a fully mutually defined fixpoint
  67. (Kinding_wf_1 and Kinding_wf_0 are not mutually dependent).
  68. Well-foundedness check may fail unexpectedly.
  69.  [non-full-mutual,fixpoints]
  70. File "./FOmega.v", line 2275, characters 0-1067:
  71. Warning: Not a fully mutually defined fixpoint
  72. (e.g., TRedStar_wf_1 and TRedStar_wf_0 are not mutually
  73. dependent).
  74. Well-foundedness check may fail unexpectedly.
  75.  [non-full-mutual,fixpoints]
  76. File "./FOmega.v", line 2293, characters 0-3034:
  77. Warning: Not a fully mutually defined fixpoint
  78. (TyEq_wf_2 and TyEq_wf_0 are not mutually dependent).
  79. Well-foundedness check may fail unexpectedly.
  80.  [non-full-mutual,fixpoints]
  81. File "./FOmega.v", line 2329, characters 0-1698:
  82. Warning: Not a fully mutually defined fixpoint
  83. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  84. Well-foundedness check may fail unexpectedly.
  85.  [non-full-mutual,fixpoints]
  86. File "./FOmega.v", line 2377, characters 0-61:
  87. Warning: obligation_Env_reg_TRed is declared as a local axiom
  88. [local-declaration,scope]
  89. COQC DeclarationEvaluation.v
  90. COQC MetaTheory.v
  91. File "./MetaTheory.v", line 281, characters 39-41:
  92. Ltac call to "exists (ne_bindings_list)" failed.
  93. Error: The reference T0 was not found in the current environment.
  94. make[2]: *** [MetaTheory.vo] Error 1
  95. make[2]: Target `all' not remade because of errors.
  96. make[1]: *** [coq] Error 2
  97. make: *** [fomega] Error 2
  98. /Library/Developer/CommandLineTools/usr/bin/make -C fsub
  99. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  100. COQC FSub.v
  101. File "./FSub.v", line 1829, characters 0-1623:
  102. Warning: Not a fully mutually defined fixpoint
  103. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  104. Well-foundedness check may fail unexpectedly.
  105.  [non-full-mutual,fixpoints]
  106. File "./FSub.v", line 1856, characters 0-57:
  107. Warning: obligation_Env_var_ty is declared as a local axiom
  108. [local-declaration,scope]
  109. File "./FSub.v", line 1870, characters 0-59:
  110. Warning: obligation_Env_reg_Sub is declared as a local axiom
  111. [local-declaration,scope]
  112. COQC DeclarationEvaluation.v
  113. COQC MetaTheory.v
  114. File "./MetaTheory.v", line 72, characters 4-5:
  115. Error: Wrong bullet + : Current bullet + is not finished.
  116. make[2]: *** [MetaTheory.vo] Error 1
  117. make[2]: Target `all' not remade because of errors.
  118. make[1]: *** [coq] Error 2
  119. make: *** [fsub] Error 2
  120. /Library/Developer/CommandLineTools/usr/bin/make -C stlc
  121. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  122. COQC Stlc.v
  123. File "./Stlc.v", line 884, characters 0-1027:
  124. Warning: Not a fully mutually defined fixpoint
  125. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  126. Well-foundedness check may fail unexpectedly.
  127.  [non-full-mutual,fixpoints]
  128. COQC DeclarationEvaluation.v
  129. COQC MetaTheory.v
  130. /Library/Developer/CommandLineTools/usr/bin/make -C fsubprod
  131. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  132. COQC FSubProd.v
  133. File "./FSubProd.v", line 2324, characters 0-1110:
  134. Warning: Not a fully mutually defined fixpoint
  135. (PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
  136. Well-foundedness check may fail unexpectedly.
  137.  [non-full-mutual,fixpoints]
  138. File "./FSubProd.v", line 2336, characters 0-2448:
  139. Warning: Not a fully mutually defined fixpoint
  140. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  141. Well-foundedness check may fail unexpectedly.
  142.  [non-full-mutual,fixpoints]
  143. File "./FSubProd.v", line 2370, characters 0-57:
  144. Warning: obligation_Env_var_ty is declared as a local axiom
  145. [local-declaration,scope]
  146. File "./FSubProd.v", line 2384, characters 0-59:
  147. Warning: obligation_Env_reg_Sub is declared as a local axiom
  148. [local-declaration,scope]
  149. COQC DeclarationEvaluation.v
  150. COQC MetaTheory.v
  151. File "./MetaTheory.v", line 100, characters 4-5:
  152. Error: Wrong bullet + : Current bullet + is not finished.
  153. make[2]: *** [MetaTheory.vo] Error 1
  154. make[2]: Target `all' not remade because of errors.
  155. make[1]: *** [coq] Error 2
  156. make: *** [fsubprod] Error 2
  157. /Library/Developer/CommandLineTools/usr/bin/make -C f
  158. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  159. COQC F.v
  160. File "./F.v", line 1670, characters 0-1402:
  161. Warning: Not a fully mutually defined fixpoint
  162. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  163. Well-foundedness check may fail unexpectedly.
  164.  [non-full-mutual,fixpoints]
  165. COQC DeclarationEvaluation.v
  166. COQC MetaTheory.v
  167. /Library/Developer/CommandLineTools/usr/bin/make -C fexists
  168. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  169. COQC Fexists.v
  170. File "./Fexists.v", line 1827, characters 0-1847:
  171. Warning: Not a fully mutually defined fixpoint
  172. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  173. Well-foundedness check may fail unexpectedly.
  174.  [non-full-mutual,fixpoints]
  175. COQC DeclarationEvaluation.v
  176. COQC MetaTheory.v
  177. /Library/Developer/CommandLineTools/usr/bin/make -C stlcprod
  178. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  179. COQC StlcProd.v
  180. File "./StlcProd.v", line 1185, characters 0-1107:
  181. Warning: Not a fully mutually defined fixpoint
  182. (PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
  183. Well-foundedness check may fail unexpectedly.
  184.  [non-full-mutual,fixpoints]
  185. File "./StlcProd.v", line 1197, characters 0-1816:
  186. Warning: Not a fully mutually defined fixpoint
  187. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  188. Well-foundedness check may fail unexpectedly.
  189.  [non-full-mutual,fixpoints]
  190. File "./StlcProd.v", line 1224, characters 0-57:
  191. Warning: obligation_Env_var_tm is declared as a local axiom
  192. [local-declaration,scope]
  193. File "./StlcProd.v", line 1232, characters 0-65:
  194. Warning: obligation_Env_reg_Typing is declared as a local axiom
  195. [local-declaration,scope]
  196. COQC DeclarationEvaluation.v
  197. COQC MetaTheory.v
  198. /Library/Developer/CommandLineTools/usr/bin/make -C fprod
  199. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  200. COQC FProd.v
  201. File "./FProd.v", line 2154, characters 0-1107:
  202. Warning: Not a fully mutually defined fixpoint
  203. (PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
  204. Well-foundedness check may fail unexpectedly.
  205.  [non-full-mutual,fixpoints]
  206. File "./FProd.v", line 2166, characters 0-2204:
  207. Warning: Not a fully mutually defined fixpoint
  208. (Typing_wf_1 and Typing_wf_0 are not mutually dependent).
  209. Well-foundedness check may fail unexpectedly.
  210.  [non-full-mutual,fixpoints]
  211. COQC DeclarationEvaluation.v
  212. COQC MetaTheory.v
  213. /Library/Developer/CommandLineTools/usr/bin/make -C fseqlet
  214. /Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
  215. COQC FSeqLet.v
  216. File "./FSeqLet.v", line 2241, characters 0-2270:
  217. Warning: Not a fully mutually defined fixpoint
  218. (Typing_wf_1 and DTyping_wf_0 are not mutually dependent).
  219. Well-foundedness check may fail unexpectedly.
  220.  [non-full-mutual,fixpoints]
  221. COQC DeclarationEvaluation.v
  222. COQC MetaTheory.v
  223. make: Target `default' not remade because of errors.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top