search

ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.
https://vericert.ymhg.org
GNU General Public License v3.0
88 stars 5 forks source link

installation issue #1

Closed johnwickerson closed 4 years ago

johnwickerson commented 4 years ago

I just tried installing coqup (master branch, 4edb75) but hit the following error:

Johns-MacBook-Pro-3:coqup jpw48$ nix-build
these derivations will be built:
  /nix/store/rwalxr271ilygq1n06680al8jckakx32-source.drv
  /nix/store/5ygvagbvihk56d5w89w6rs23l2wqhqcf-coq8.10-bbv.drv
  /nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv
these paths will be fetched (322.92 MiB download, 1581.04 MiB unpacked):
  /nix/store/009k5a1n92lrav4fh2xnz23qf2jrh7jm-patch-2.7.6
  /nix/store/08nipyxbag0vwsjs6fafvndlinm510gj-llvm-7.1.0
  /nix/store/0c288xy3i4g6c38aa067ixa5mb9lk0lf-nghttp2-1.40.0-lib
  /nix/store/0mmgv39ij03kw12znr0pkjyvawnjf4wd-zlib-1.2.11-dev
  /nix/store/12swncflm8b1nif8cfzalchki6qfdf05-stdenv-darwin
  /nix/store/1ngwf6wvh9hf1vz3h2h5znqi90fa86q1-clang-wrapper-7.1.0
  /nix/store/1q222g8p6dhjvdkhgn4vydxhx1mhbi9f-libev-4.33
  /nix/store/1xn77yix5qbxy49w734js17hyjag0vm5-unzip-6.0
  /nix/store/23fhqc2b3yqbgk2h62dnqzyhq1g8pvg8-coq-8.10.2
  /nix/store/25x2pjx54r34cklwj15mmbkc8zxk7wjn-c-ares-1.15.0
  /nix/store/2vlb0jnsz5v6w3c1q3clgzfxd47shlkz-curl-7.68.0-dev
  /nix/store/2zyg3d8hcgqn4sv7cc9k41sy49yjggdn-curl-7.68.0-man
  /nix/store/3anjymbdrfcf5sqyq3zdmb5mnkrfnv3v-nghttp2-1.40.0-dev
  /nix/store/3b5092bc3xa5gxwr4sxkvh3b9d4iypz2-clang-7.1.0-lib
  /nix/store/47m4h1bb5df8k6031qbljfr4w3m63f68-libc++-7.1.0
  /nix/store/4fxk0lf2zy3ib7488fh7573naa53jq37-xz-5.2.5
  /nix/store/4m1zvi1rmjf32rwqqmwsa4v181nfvycb-expand-response-params
  /nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23
  /nix/store/4q0y4pbgc82lj7llxwj5n6ly2xsc5hm7-openssl-1.1.1d-dev
  /nix/store/6wf9n219synck5gbkrk0zrb9qg4bgz3c-bzip2-1.0.6.0.1-bin
  /nix/store/7955xrl5hg078v0ip0ki8wnm7kqx44kl-ncurses-6.2-dev
  /nix/store/7j9543gj0idrcimyxg9rkfdnkcgav3bp-gettext-0.20.1
  /nix/store/7x9a14vrl2mfrg89nhik3vq8z086lq1y-gfortran-9.3.0-lib
  /nix/store/7y6vn8wr00zwkcnv830qjkra37gvd11p-gettext-0.20.1
  /nix/store/7zryalm91s9im117zvq1hcgzs42al0g7-libiconv-osx-10.12.6
  /nix/store/81rb87agmp9cbsvg2xm2n4kp9c6309lv-ncurses-6.2
  /nix/store/87bk6piv948k764i0cin48vhv9s1ymn9-nghttp2-1.40.0-bin
  /nix/store/88z08d33mc8ymkxv006zp43lagdr327j-ocaml-4.09.1
  /nix/store/8r83yw77k1cbpcbvvwiwxi047rgiba6r-gcc-wrapper-9.3.0
  /nix/store/8z9kzsdjyncfq51whxlihbnkz8f16vy5-bzip2-1.0.6.0.1
  /nix/store/951rfqjj70an91lwzz7lwz67rg8yzxfz-menhir-20190626
  /nix/store/9bvvaa06570pib2c9p8m2rjb47fsrfs5-libffi-3.3
  /nix/store/9in7vl1f3dyis8k3kyc6qc9vsgg8735m-stdenv-darwin
  /nix/store/a79h3hc5izpxkrpafc1g4kkzb22yl7is-zlib-1.2.11
  /nix/store/a8dl27c6phbd9g2ml7yycyljn00v3x97-xz-5.2.5-bin
  /nix/store/ayn43f7la4dacipvbd2r9q373bspv3y5-openssl-1.1.1d-bin
  /nix/store/bak7c725z70hwwfjx14zvgxyd109zz41-expand-response-params
  /nix/store/c19aq0fh668s6q5pha75my8wmndpzfxf-dune-1.11.4
  /nix/store/d66n620h6mzdsrwksjs1ik7w3s42107b-libssh2-1.9.0
  /nix/store/f9rirp60zkzin9cxp4a4d2c3pvw8n027-compiler-rt-7.1.0
  /nix/store/fb1cjkwb8bha530wabxxqn32xzijgjw8-gmp-6.2.0
  /nix/store/fxplyfw6p0xrp61m6mhaxxil2br00kfp-llvm-7.1.0-lib
  /nix/store/gc46vimya56ss3lncapw7sdn5z0162l3-curl-7.68.0
  /nix/store/gnqq3wkfcbcryjmwkaxndw2g4xgamygv-binutils-2.31.1
  /nix/store/gw3ygl9rya28a74jv99bky9xzg04h0hx-gawk-5.0.1
  /nix/store/hgb8ykjhfk05fiwshz5ial6v83j0ssqb-ocaml-findlib-1.8.1
  /nix/store/hj85vcq46xk7x3ijk2w4x3kbjl6r7xa1-gcc-9.3.0-lib
  /nix/store/hz71p4lbzhn90vi9yacxyw42b5baiyl2-coreutils-8.31
  /nix/store/i5p6snm3s4wmmbif4fkjjaqlaycj8fm5-Libsystem-osx-10.12.6
  /nix/store/iv6rwmig8275lhds5n62k3w9cqwv3fpj-nghttp2-1.40.0-lib
  /nix/store/j53wgkqy59pih1w8pz44hskhrivnz3jh-libkrb5-1.18
  /nix/store/jhzqb2ar196ah8ar8wa3l703x15jbbsd-libssh2-1.9.0-dev
  /nix/store/jlhva5dy674rm4w91bbnyip2p6ij7wa1-swift-corefoundation
  /nix/store/jnkg82sd6kv22iaccgq79h86wdpryja5-gnutar-1.32
  /nix/store/jsspspmr3cm0b9w7gc365d2ppq8kk7x1-compiler-rt-7.1.0-dev
  /nix/store/jswqkbfhaf27nwbch4x6afmba40j46l5-openssl-1.1.1d
  /nix/store/nccijbipzpw4y6jkyr6h22jjwqhhnh6r-mpfr-4.0.2
  /nix/store/nfb90w47wml828m8bycykhd7gfbql3if-nghttp2-1.40.0
  /nix/store/nqsqc671iw4ngzlf1s40s7iy9vf5flk7-gzip-1.10
  /nix/store/p26faqrnlkwynjdrgl5ng6j4a3s1h1rk-pcre-8.44
  /nix/store/pg5q1mhsfmbk9sn5yagvzbd0dfhr737k-curl-7.68.0
  /nix/store/pk869gvnslszr8f0k9k1209pgfd8mpm3-libmpc-1.1.0
  /nix/store/q6vcxyrr0anr6hc8hwvx7jjbp7ci0z3k-ICU-osx-10.10.5
  /nix/store/qj4y7q0pb9cc9wjwk4dmvbx53d2kwpq4-gnumake-4.2.1
  /nix/store/qjfcs4kbq33qndybdizpp7xrsdx43px9-libxml2-2.9.10
  /nix/store/r5nwlqrwqkpx85hhf1q5j1jkgfvmk7gc-diffutils-3.7
  /nix/store/r8136nw2x3s2yhrbiq5p26lz62xrj5j3-cctools-port
  /nix/store/rxmf15h0n4gglfiza4rxqif49rv25nzc-libc++abi-7.1.0
  /nix/store/s0zdf9c8v3421b4qndp5npfbzf4h4pll-camlp5-7.11
  /nix/store/s2gpzzixrm9xmzym2py4w1zln4dr2hgh-gcc-9.3.0
  /nix/store/v1pa6217x3yi6gms06y6xqnc48dayqb4-gnused-4.8
  /nix/store/v8561qp6ifmblkc8q2xsig9dl8c3sfj4-adv_cmds-osx-10.5.8-locale
  /nix/store/vbv17cmdp71q6n9lvy1bwlf23ccb4va9-mirrors-list
  /nix/store/vs07zwi9mnqrcrinrggfb5n465i8y6wp-libssh2-1.9.0
  /nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2
  /nix/store/w4p33hisv8rxig7b506806j5djdk5lkn-openssl-1.1.1d
  /nix/store/w4vj07i9cq1g9vg9y0l44ijy80k9hlwz-findutils-4.7.0
  /nix/store/w78a567dc5phiy7f1xvyim62d6wlydal-cctools-binutils-darwin-wrapper-927.0.2
  /nix/store/w7sfzkp1j8vxby846jls0m560hj7rmmg-blas-3.8.0
  /nix/store/x9mz63vfknb076bqv06simqsb003vq32-curl-7.68.0-bin
  /nix/store/xbd074qa4p62sjbcmkvbzrb1d4zcj79n-clang-7.1.0
  /nix/store/xqn9fppqna4p71lwjnndq6bsv3pb7h5q-csdp-6.1.1
  /nix/store/ych43swl3x9p4brm27kpchpqa8jpal4x-ed-1.16
  /nix/store/z3d9cpkfr8y9j44jarmw56i193f6j27j-ncurses-6.2-man
  /nix/store/zak500ybyjk4yiqm6yxcxs418jpi80v4-gnugrep-3.4
copying path '/nix/store/i5p6snm3s4wmmbif4fkjjaqlaycj8fm5-Libsystem-osx-10.12.6' from 'https://cache.nixos.org'...
copying path '/nix/store/v8561qp6ifmblkc8q2xsig9dl8c3sfj4-adv_cmds-osx-10.5.8-locale' from 'https://cache.nixos.org'...
copying path '/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23' from 'https://cache.nixos.org'...
copying path '/nix/store/8z9kzsdjyncfq51whxlihbnkz8f16vy5-bzip2-1.0.6.0.1' from 'https://cache.nixos.org'...
copying path '/nix/store/2zyg3d8hcgqn4sv7cc9k41sy49yjggdn-curl-7.68.0-man' from 'https://cache.nixos.org'...
copying path '/nix/store/6wf9n219synck5gbkrk0zrb9qg4bgz3c-bzip2-1.0.6.0.1-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/ych43swl3x9p4brm27kpchpqa8jpal4x-ed-1.16' from 'https://cache.nixos.org'...
copying path '/nix/store/4m1zvi1rmjf32rwqqmwsa4v181nfvycb-expand-response-params' from 'https://cache.nixos.org'...
copying path '/nix/store/gw3ygl9rya28a74jv99bky9xzg04h0hx-gawk-5.0.1' from 'https://cache.nixos.org'...
copying path '/nix/store/qj4y7q0pb9cc9wjwk4dmvbx53d2kwpq4-gnumake-4.2.1' from 'https://cache.nixos.org'...
copying path '/nix/store/v1pa6217x3yi6gms06y6xqnc48dayqb4-gnused-4.8' from 'https://cache.nixos.org'...
copying path '/nix/store/nqsqc671iw4ngzlf1s40s7iy9vf5flk7-gzip-1.10' from 'https://cache.nixos.org'...
copying path '/nix/store/rxmf15h0n4gglfiza4rxqif49rv25nzc-libc++abi-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/9bvvaa06570pib2c9p8m2rjb47fsrfs5-libffi-3.3' from 'https://cache.nixos.org'...
copying path '/nix/store/47m4h1bb5df8k6031qbljfr4w3m63f68-libc++-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7zryalm91s9im117zvq1hcgzs42al0g7-libiconv-osx-10.12.6' from 'https://cache.nixos.org'...
copying path '/nix/store/q6vcxyrr0anr6hc8hwvx7jjbp7ci0z3k-ICU-osx-10.10.5' from 'https://cache.nixos.org'...
copying path '/nix/store/r8136nw2x3s2yhrbiq5p26lz62xrj5j3-cctools-port' from 'https://cache.nixos.org'...
copying path '/nix/store/f9rirp60zkzin9cxp4a4d2c3pvw8n027-compiler-rt-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7j9543gj0idrcimyxg9rkfdnkcgav3bp-gettext-0.20.1' from 'https://cache.nixos.org'...
copying path '/nix/store/jsspspmr3cm0b9w7gc365d2ppq8kk7x1-compiler-rt-7.1.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/fb1cjkwb8bha530wabxxqn32xzijgjw8-gmp-6.2.0' from 'https://cache.nixos.org'...
copying path '/nix/store/jnkg82sd6kv22iaccgq79h86wdpryja5-gnutar-1.32' from 'https://cache.nixos.org'...
copying path '/nix/store/hz71p4lbzhn90vi9yacxyw42b5baiyl2-coreutils-8.31' from 'https://cache.nixos.org'...
copying path '/nix/store/j53wgkqy59pih1w8pz44hskhrivnz3jh-libkrb5-1.18' from 'https://cache.nixos.org'...
copying path '/nix/store/r5nwlqrwqkpx85hhf1q5j1jkgfvmk7gc-diffutils-3.7' from 'https://cache.nixos.org'...
copying path '/nix/store/w4vj07i9cq1g9vg9y0l44ijy80k9hlwz-findutils-4.7.0' from 'https://cache.nixos.org'...
copying path '/nix/store/vbv17cmdp71q6n9lvy1bwlf23ccb4va9-mirrors-list' from 'https://cache.nixos.org'...
copying path '/nix/store/81rb87agmp9cbsvg2xm2n4kp9c6309lv-ncurses-6.2' from 'https://cache.nixos.org'...
copying path '/nix/store/z3d9cpkfr8y9j44jarmw56i193f6j27j-ncurses-6.2-man' from 'https://cache.nixos.org'...
copying path '/nix/store/nfb90w47wml828m8bycykhd7gfbql3if-nghttp2-1.40.0' from 'https://cache.nixos.org'...
copying path '/nix/store/7955xrl5hg078v0ip0ki8wnm7kqx44kl-ncurses-6.2-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/0c288xy3i4g6c38aa067ixa5mb9lk0lf-nghttp2-1.40.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/jswqkbfhaf27nwbch4x6afmba40j46l5-openssl-1.1.1d' from 'https://cache.nixos.org'...
copying path '/nix/store/009k5a1n92lrav4fh2xnz23qf2jrh7jm-patch-2.7.6' from 'https://cache.nixos.org'...
copying path '/nix/store/p26faqrnlkwynjdrgl5ng6j4a3s1h1rk-pcre-8.44' from 'https://cache.nixos.org'...
copying path '/nix/store/4fxk0lf2zy3ib7488fh7573naa53jq37-xz-5.2.5' from 'https://cache.nixos.org'...
copying path '/nix/store/zak500ybyjk4yiqm6yxcxs418jpi80v4-gnugrep-3.4' from 'https://cache.nixos.org'...
copying path '/nix/store/a8dl27c6phbd9g2ml7yycyljn00v3x97-xz-5.2.5-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/a79h3hc5izpxkrpafc1g4kkzb22yl7is-zlib-1.2.11' from 'https://cache.nixos.org'...
copying path '/nix/store/gnqq3wkfcbcryjmwkaxndw2g4xgamygv-binutils-2.31.1' from 'https://cache.nixos.org'...
copying path '/nix/store/vs07zwi9mnqrcrinrggfb5n465i8y6wp-libssh2-1.9.0' from 'https://cache.nixos.org'...
copying path '/nix/store/qjfcs4kbq33qndybdizpp7xrsdx43px9-libxml2-2.9.10' from 'https://cache.nixos.org'...
copying path '/nix/store/gc46vimya56ss3lncapw7sdn5z0162l3-curl-7.68.0' from 'https://cache.nixos.org'...
copying path '/nix/store/fxplyfw6p0xrp61m6mhaxxil2br00kfp-llvm-7.1.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/jlhva5dy674rm4w91bbnyip2p6ij7wa1-swift-corefoundation' from 'https://cache.nixos.org'...
copying path '/nix/store/3b5092bc3xa5gxwr4sxkvh3b9d4iypz2-clang-7.1.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/25x2pjx54r34cklwj15mmbkc8zxk7wjn-c-ares-1.15.0' from 'https://cache.nixos.org'...
copying path '/nix/store/xbd074qa4p62sjbcmkvbzrb1d4zcj79n-clang-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/bak7c725z70hwwfjx14zvgxyd109zz41-expand-response-params' from 'https://cache.nixos.org'...
copying path '/nix/store/7y6vn8wr00zwkcnv830qjkra37gvd11p-gettext-0.20.1' from 'https://cache.nixos.org'...
copying path '/nix/store/1q222g8p6dhjvdkhgn4vydxhx1mhbi9f-libev-4.33' from 'https://cache.nixos.org'...
copying path '/nix/store/hj85vcq46xk7x3ijk2w4x3kbjl6r7xa1-gcc-9.3.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/7x9a14vrl2mfrg89nhik3vq8z086lq1y-gfortran-9.3.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/nccijbipzpw4y6jkyr6h22jjwqhhnh6r-mpfr-4.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/w7sfzkp1j8vxby846jls0m560hj7rmmg-blas-3.8.0' from 'https://cache.nixos.org'...
copying path '/nix/store/pk869gvnslszr8f0k9k1209pgfd8mpm3-libmpc-1.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/xqn9fppqna4p71lwjnndq6bsv3pb7h5q-csdp-6.1.1' from 'https://cache.nixos.org'...
copying path '/nix/store/s2gpzzixrm9xmzym2py4w1zln4dr2hgh-gcc-9.3.0' from 'https://cache.nixos.org'...
copying path '/nix/store/iv6rwmig8275lhds5n62k3w9cqwv3fpj-nghttp2-1.40.0-lib' from 'https://cache.nixos.org'...
copying path '/nix/store/88z08d33mc8ymkxv006zp43lagdr327j-ocaml-4.09.1' from 'https://cache.nixos.org'...
copying path '/nix/store/w4p33hisv8rxig7b506806j5djdk5lkn-openssl-1.1.1d' from 'https://cache.nixos.org'...
copying path '/nix/store/s0zdf9c8v3421b4qndp5npfbzf4h4pll-camlp5-7.11' from 'https://cache.nixos.org'...
copying path '/nix/store/c19aq0fh668s6q5pha75my8wmndpzfxf-dune-1.11.4' from 'https://cache.nixos.org'...
copying path '/nix/store/d66n620h6mzdsrwksjs1ik7w3s42107b-libssh2-1.9.0' from 'https://cache.nixos.org'...
copying path '/nix/store/951rfqjj70an91lwzz7lwz67rg8yzxfz-menhir-20190626' from 'https://cache.nixos.org'...
copying path '/nix/store/pg5q1mhsfmbk9sn5yagvzbd0dfhr737k-curl-7.68.0' from 'https://cache.nixos.org'...
copying path '/nix/store/jhzqb2ar196ah8ar8wa3l703x15jbbsd-libssh2-1.9.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/x9mz63vfknb076bqv06simqsb003vq32-curl-7.68.0-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/87bk6piv948k764i0cin48vhv9s1ymn9-nghttp2-1.40.0-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/hgb8ykjhfk05fiwshz5ial6v83j0ssqb-ocaml-findlib-1.8.1' from 'https://cache.nixos.org'...
copying path '/nix/store/3anjymbdrfcf5sqyq3zdmb5mnkrfnv3v-nghttp2-1.40.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/23fhqc2b3yqbgk2h62dnqzyhq1g8pvg8-coq-8.10.2' from 'https://cache.nixos.org'...
copying path '/nix/store/ayn43f7la4dacipvbd2r9q373bspv3y5-openssl-1.1.1d-bin' from 'https://cache.nixos.org'...
copying path '/nix/store/9in7vl1f3dyis8k3kyc6qc9vsgg8735m-stdenv-darwin' from 'https://cache.nixos.org'...
copying path '/nix/store/4q0y4pbgc82lj7llxwj5n6ly2xsc5hm7-openssl-1.1.1d-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/1xn77yix5qbxy49w734js17hyjag0vm5-unzip-6.0' from 'https://cache.nixos.org'...
copying path '/nix/store/0mmgv39ij03kw12znr0pkjyvawnjf4wd-zlib-1.2.11-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/2vlb0jnsz5v6w3c1q3clgzfxd47shlkz-curl-7.68.0-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/08nipyxbag0vwsjs6fafvndlinm510gj-llvm-7.1.0' from 'https://cache.nixos.org'...
building '/nix/store/rwalxr271ilygq1n06680al8jckakx32-source.drv'...

trying https://github.com/mit-plv/bbv/archive/5099237c52d2910f79a1a3ca9ae4dfa80129bf86.tar.gz
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   153  100   153    0     0    993      0 --:--:-- --:--:-- --:--:--   993
100 51982    0 51982    0     0  71997      0 --:--:-- --:--:-- --:--:--  135k
unpacking source archive /private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-source.drv-0/5099237c52d2910f79a1a3ca9ae4dfa80129bf86.tar.gz
copying path '/nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/w78a567dc5phiy7f1xvyim62d6wlydal-cctools-binutils-darwin-wrapper-927.0.2' from 'https://cache.nixos.org'...
copying path '/nix/store/1ngwf6wvh9hf1vz3h2h5znqi90fa86q1-clang-wrapper-7.1.0' from 'https://cache.nixos.org'...
copying path '/nix/store/8r83yw77k1cbpcbvvwiwxi047rgiba6r-gcc-wrapper-9.3.0' from 'https://cache.nixos.org'...
copying path '/nix/store/12swncflm8b1nif8cfzalchki6qfdf05-stdenv-darwin' from 'https://cache.nixos.org'...
building '/nix/store/5ygvagbvihk56d5w89w6rs23l2wqhqcf-coq8.10-bbv.drv'...
unpacking sources
unpacking source archive /nix/store/98phrsgw9p8qhwp30ch81r6bqmjnhx6v-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
build flags: -j4 -l4 SHELL=/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash
coq_makefile -f _CoqProject ./src/bbv/NLib.v ./src/bbv/DepEq.v ./src/bbv/BinNotationZ.v ./src/bbv/Nomega.v ./src/bbv/NatLib.v ./src/bbv/ZLib.v ./src/bbv/DepEqNat.v ./src/bbv/ReservedNotations.v ./src/bbv/HexNotation.v ./src/bbv/BinNotation.v ./src/bbv/HexNotationZ.v ./src/bbv/WordScope.v ./src/bbv/ZHints.v ./src/bbv/Word.v ./src/bbv/HexNotationWord.v ./src/bbv/N_Z_nat_conversions.v -o Makefile.coq.all
make -f Makefile.coq.all
make[1]: Entering directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
COQDEP VFILES
COQC src/bbv/NLib.v
COQC src/bbv/ReservedNotations.v
COQC src/bbv/Nomega.v
COQC src/bbv/N_Z_nat_conversions.v
COQC src/bbv/ZLib.v
COQC src/bbv/DepEqNat.v
COQC src/bbv/HexNotation.v
COQC src/bbv/ZHints.v
COQC src/bbv/NatLib.v
COQC src/bbv/HexNotationZ.v
COQC src/bbv/BinNotation.v
COQC src/bbv/DepEq.v
COQC src/bbv/BinNotationZ.v
COQC src/bbv/Word.v
File "./src/bbv/Word.v", line 27, characters 0-35:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope word_scope.". [undeclared-scope,deprecated]
File "./src/bbv/Word.v", line 155, characters 0-28:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 446, characters 0-45:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 1136, characters 0-43:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 1268, characters 0-42:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./src/bbv/Word.v", line 2265, characters 0-28:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC src/bbv/WordScope.v
COQC src/bbv/HexNotationWord.v
make[1]: Leaving directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
installing
INSTALL ./src/bbv/NLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.vo /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.v /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEq.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotationZ.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Nomega.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/NatLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZLib.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/DepEqNat.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ReservedNotations.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotation.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/BinNotation.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationZ.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/WordScope.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/ZHints.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/Word.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/HexNotationWord.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
INSTALL ./src/bbv/N_Z_nat_conversions.glob /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib/coq/8.10//user-contrib/bbv/
make[1]: Entering directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
make[1]: Leaving directory '/private/var/folders/js/z_kj2f215t9844dczy96r_hr0000gn/T/nix-build-coq8.10-bbv.drv-0/source'
post-installation fixup
strip is /nix/store/w03sx2iyra2is64ybjn6ps1kw2gaqvw0-cctools-binutils-darwin-927.0.2/bin/strip
stripping (with command strip and flags -S) in /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv/lib 
patching script interpreter paths in /nix/store/z90q659qs808wm38niyi0v0a5irhbkmb-coq8.10-bbv
building '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv'...
unpacking sources
unpacking source archive /nix/store/mplhq2zjqgmag56sl09j7c0az37czg4s-coqup
source root is coqup
patching sources
configuring
no configure script, doing nothing
building
build flags: -j4 -l4 SHELL=/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash
(cd lib/CompCert && ./configure x86_64-linux)
/nix/store/4p3bds5cknzwg72np1rzyn3jq0962z84-bash-4.4-p23/bin/bash: ./configure: No such file or directory
make: *** [Makefile:26: lib/COMPCERTSTAMP] Error 127
builder for '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv' failed with exit code 2
error: build of '/nix/store/l55gwij4yy7bw725lyvwh6awx2fgba5l-coqup.drv' failed
ymherklotz commented 4 years ago

Oh sorry, I think CompCert might not have downloaded properly. To clone the repo, I should have added that you need to use the following command:

git clone --recursive https://github.com/ymherklotz/coqup

However, in the github repo, if you run:

git submodule update --init

It should download CompCert.

In addition to that, if you are building it on MacOSx, you have to change a line in the makefile. I believe it is line 22, change:

(cd lib/CompCert && ./configure x86_64-linux)

to

(cd lib/CompCert && ./configure x86_64-macosx)

Finally, currently nix-build is a bit broken, it will build correctly but delete the binary, so an easier way to test is the following

nix-shell  # downloads all dependencies
make -j8  # Build compcert and coqup
make install  # Install binary in current directory, under ./bin/coqup
./bin/coqup -o main.v main.c  # To build a C file

Hope that helps, I'll improve the instructions in the readme.

johnwickerson commented 4 years ago

Thanks. The examples all compile fine now!