Diff of the two buildlogs: -- --- b1/build.log 2024-12-19 08:31:28.756291017 +0000 +++ b2/build.log 2024-12-19 08:34:04.425231218 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Jan 21 02:52:02 -12 2026 -I: pbuilder-time-stamp: 1769007122 +I: Current time: Thu Dec 19 22:31:31 +14 2024 +I: pbuilder-time-stamp: 1734597091 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -28,51 +28,83 @@ dpkg-source: info: applying 0001-Increase-timeout-in-test-that-takes-a-bit-longer-on-.patch I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3008132/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/D01_modify_environment starting +debug: Running on infom01-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Dec 19 08:31 /bin/sh -> /bin/bash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="37" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.37(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='trixie' - HOME='/root' - HOST_ARCH='amd64' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='39cbe2f7cdf54194bfd06e7f366f0f4c' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='3008132' - PS1='# ' - PS2='> ' + INVOCATION_ID=ab4b4d7f9fa04f67afcd48e99e35df65 + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=761097 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.vhEjciJp/pbuilderrc_PSA1 --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.vhEjciJp/b1 --logfile b1/build.log coq-elpi_2.2.3-1.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.vhEjciJp/pbuilderrc_z4HZ --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.vhEjciJp/b2 --logfile b2/build.log coq-elpi_2.2.3-1.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' I: uname -a - Linux infom02-amd64 6.11.5+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.11.5-1~bpo12+1 (2024-11-11) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-28-cloud-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.119-1 (2024-11-22) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/3008132/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -219,7 +251,7 @@ Get: 93 http://deb.debian.org/debian trixie/main amd64 libstdio-ocaml-dev amd64 0.17.0-1 [116 kB] Get: 94 http://deb.debian.org/debian trixie/main amd64 libppx-optcomp-ocaml-dev amd64 1:0.17.0-1+b3 [327 kB] Get: 95 http://deb.debian.org/debian trixie/main amd64 ocaml-dune amd64 3.16.0-2+b1 [4786 kB] -Fetched 378 MB in 3s (132 MB/s) +Fetched 378 MB in 4s (100 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.12-minimal:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19959 files and directories currently installed.) @@ -542,8 +574,8 @@ Setting up tzdata (2024b-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Jan 21 14:53:04 UTC 2026. -Universal Time is now: Wed Jan 21 14:53:04 UTC 2026. +Local time is now: Thu Dec 19 08:32:51 UTC 2024. +Universal Time is now: Thu Dec 19 08:32:51 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -628,7 +660,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-elpi-2.2.3/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-elpi_2.2.3-1_source.changes +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-elpi-2.2.3/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../coq-elpi_2.2.3-1_source.changes dpkg-buildpackage: info: source package coq-elpi dpkg-buildpackage: info: source version 2.2.3-1 dpkg-buildpackage: info: source distribution unstable @@ -678,8 +714,6 @@ (Build bool false 3 eq_refl eq_refl) = 3 example_import_projections.f1 _ x : bool -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_generalize.v) -3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_fuzzer.v) DEBUG: attempt at fuzzing binary op: global (indc «PLUS») DEBUG: attempt at fuzzing binary op: global (const «Nat.add») @@ -726,6 +760,8 @@ (forall t : f1, f2 t -> bool) -> foo Arguments mk_foo f1%type_scope (f2 f3)%function_scope +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_generalize.v) +3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_reduction_surgery.v) (eq_refl : 2 = (let z := 1 in S z)) (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_record_expansion.v) @@ -788,6 +824,15 @@ prod `_` (app [global (const «lt»), c1, c2]) c4 \ app [global (const «lt»), c0, c2] 3 +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_data_base.v) +The Db contains [phone_prefix USA 1] +Phone prefix for USA is 1 +The Db contains +[phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39] +Phone prefix for France is 33 +sweet! +brr +yummy! (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_reflexive_tactic.v) normP : forall {T : Type} {e : T} {op : T -> T -> T} {gamma : list T} {t1 t2 : lang}, @@ -811,102 +856,6 @@ Debug: In environment x, y, z, t : Z Unable to unify "var 1" with "var 0". -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_data_base.v) -The Db contains [phone_prefix USA 1] -Phone prefix for USA is 1 -The Db contains -[phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39] -Phone prefix for France is 33 -sweet! -brr -yummy! -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_command.v) -Hello [str world!] -Hello [int 46] -Hello [str there] -Hello [str my, str friend] -Hello [str this.is.a.qualified.name] -Hello -[trm - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])] -Hello -[const-decl test - (some - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] -Hello -[indt-decl - (record test (sort (typ «Set»)) Build_test - (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ - field [coercion off, canonical tt] f2 - (app - [global (indt «eq»), global (indt «nat»), c0, - app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] -The type of -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], global (indc «O»)] is -sort prop -1 = true - : Prop -T= -app - [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], - global (indc «true»)] -T1= -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], - app [global (const «bool2nat»), global (indc «true»)]] -Ty= sort prop -nK_bool = 2 - : nat -nK_False = 0 - : nat -Inductive tree' (A : Set) : Set := - leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. - -Arguments tree' A%type_scope -Arguments leaf' A%type_scope -Arguments node' A%type_scope _ _ _ -bob is 24 years old -alice is 21 years old -bob is 24 years old -alice is 21 years old -[attribute elpi.loc - (leaf-loc - File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), - attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), - attribute more (node [attribute stuff (leaf-str 33)])] -options= -[get-option elpi.loc - File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, - get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] -33 tt -That is all folks! -going from source to target via plane -synterp x := some _ -interp x := -some - (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) -The module is «elpi_examples.tutorial_coq_elpi_command.Module46» -Box.Box.Box.Box.foo = fun n : nat => n + 2 - : nat -> nat - -Arguments Box.Box.Box.Box.foo n%nat_scope -Module NextModule2 := Struct End -File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: -Warning: This command does not support this attribute: unknown. -[unsupported-attributes,parsing,default] (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_elpi_lang.v) The age of alice is 20 Query assignments: @@ -1500,6 +1449,93 @@ A = X0 B = X0 C = X0 +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_command.v) +Hello [str world!] +Hello [int 46] +Hello [str there] +Hello [str my, str friend] +Hello [str this.is.a.qualified.name] +Hello +[trm + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])] +Hello +[const-decl test + (some + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] +Hello +[indt-decl + (record test (sort (typ «Set»)) Build_test + (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ + field [coercion off, canonical tt] f2 + (app + [global (indt «eq»), global (indt «nat»), c0, + app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] +The type of +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], global (indc «O»)] is +sort prop +1 = true + : Prop +T= +app + [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], + global (indc «true»)] +T1= +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], + app [global (const «bool2nat»), global (indc «true»)]] +Ty= sort prop +nK_bool = 2 + : nat +nK_False = 0 + : nat +Inductive tree' (A : Set) : Set := + leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. + +Arguments tree' A%type_scope +Arguments leaf' A%type_scope +Arguments node' A%type_scope _ _ _ +bob is 24 years old +alice is 21 years old +bob is 24 years old +alice is 21 years old +[attribute elpi.loc + (leaf-loc + File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), + attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), + attribute more (node [attribute stuff (leaf-str 33)])] +options= +[get-option elpi.loc + File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, + get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] +33 tt +That is all folks! +going from source to target via plane +synterp x := some _ +interp x := +some + (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) +The module is «elpi_examples.tutorial_coq_elpi_command.Module45» +Box.Box.Box.Box.foo = fun n : nat => n + 2 + : nat -> nat + +Arguments Box.Box.Box.Box.foo n%nat_scope +Module NextModule2 := Struct End +File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: +Warning: This command does not support this attribute: unknown. +[unsupported-attributes,parsing,default] (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_HOAS.v) Query assignments: GRnat = indt «nat» @@ -2322,6 +2358,18 @@ ^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Library.indirect_accessor Most commands should not be accessing opaque data. +foo = +{f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} + : Type +mk_foo = +fun (f1 : Type) (f2 : f1 -> Type) (f3 : forall t : f1, f2 t -> bool) => +existT (fun f4 : Type => {f5 : f4 -> Type & forall t : f4, f5 t -> bool}) f1 + (existT (fun f4 : f1 -> Type => forall t : f1, f4 t -> bool) f2 f3) + : forall (f1 : Type) (f2 : f1 -> Type), + (forall t : f1, f2 t -> bool) -> foo + +Arguments mk_foo f1%type_scope (f2 f3)%function_scope +3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) Notation p2 := (p2 nat 3 x) example_import_projections.p1 nat 3 x : nat : nat @@ -2335,7 +2383,7 @@ (Build bool false 3 eq_refl eq_refl) = 3 example_import_projections.f1 _ x : bool -3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) +(eq_refl : 2 = (let z := 1 in S z)) DEBUG: attempt at fuzzing binary op: global (indc «PLUS») DEBUG: attempt at fuzzing binary op: global (const «Nat.add») DEBUG: attempt at fuzzing binary op: global (indc «AND») @@ -2369,28 +2417,6 @@ Arguments E_AND1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_OR1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_EQ1 e1 e2 (n1 n2)%nat_scope _ _ -(eq_refl : 2 = (let z := 1 in S z)) -foo = -{f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} - : Type -mk_foo = -fun (f1 : Type) (f2 : f1 -> Type) (f3 : forall t : f1, f2 t -> bool) => -existT (fun f4 : Type => {f5 : f4 -> Type & forall t : f4, f5 t -> bool}) f1 - (existT (fun f4 : f1 -> Type => forall t : f1, f4 t -> bool) f2 f3) - : forall (f1 : Type) (f2 : f1 -> Type), - (forall t : f1, f2 t -> bool) -> foo - -Arguments mk_foo f1%type_scope (f2 f3)%function_scope -goal X0 c0 c1 c2 c3 is - -[decl c3 `H` (app [global (const «lt»), c0, c1]), - decl c2 `z` (global (indt «nat»)), decl c1 `y` (global (indt «nat»)), - decl c0 `x` (global (indt «nat»))] -------- - -prod `_` (app [global (const «lt»), c1, c2]) c4 \ - app [global (const «lt»), c0, c2] -3 f = fun (b : bool) (t : r) => let q := negb b in @@ -2439,6 +2465,16 @@ Arguments expanded_g T%type_scope op%function_scope (l s)%list_scope h%bool_scope +goal X0 c0 c1 c2 c3 is + +[decl c3 `H` (app [global (const «lt»), c0, c1]), + decl c2 `z` (global (indt «nat»)), decl c1 `y` (global (indt «nat»)), + decl c0 `x` (global (indt «nat»))] +------- + +prod `_` (app [global (const «lt»), c1, c2]) c4 \ + app [global (const «lt»), c0, c2] +3 The Db contains [phone_prefix USA 1] Phone prefix for USA is 1 The Db contains @@ -3075,6 +3111,92 @@ A = X0 B = X0 C = X0 +Hello [str world!] +Hello [int 46] +Hello [str there] +Hello [str my, str friend] +Hello [str this.is.a.qualified.name] +Hello +[trm + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])] +Hello +[const-decl test + (some + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] +Hello +[indt-decl + (record test (sort (typ «Set»)) Build_test + (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ + field [coercion off, canonical tt] f2 + (app + [global (indt «eq»), global (indt «nat»), c0, + app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] +The type of +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], global (indc «O»)] is +sort prop +1 = true + : Prop +T= +app + [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], + global (indc «true»)] +T1= +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], + app [global (const «bool2nat»), global (indc «true»)]] +Ty= sort prop +nK_bool = 2 + : nat +nK_False = 0 + : nat +Inductive tree' (A : Set) : Set := + leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. + +Arguments tree' A%type_scope +Arguments leaf' A%type_scope +Arguments node' A%type_scope _ _ _ +bob is 24 years old +alice is 21 years old +bob is 24 years old +alice is 21 years old +[attribute elpi.loc + (leaf-loc + File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), + attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), + attribute more (node [attribute stuff (leaf-str 33)])] +options= +[get-option elpi.loc + File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, + get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] +33 tt +That is all folks! +going from source to target via plane +synterp x := some _ +interp x := +some + (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) +The module is «elpi_examples.tutorial_coq_elpi_command.Module46» +Box.Box.Box.Box.foo = fun n : nat => n + 2 + : nat -> nat + +Arguments Box.Box.Box.Box.foo n%nat_scope +Module NextModule2 := Struct End +File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: +Warning: This command does not support this attribute: unknown. +[unsupported-attributes,parsing,default] Query assignments: GRnat = indt «nat» GRplus = const «Nat.add» @@ -3428,92 +3550,6 @@ _uvk_21_ = X0 Syntactic constraints: evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */ -Hello [str world!] -Hello [int 46] -Hello [str there] -Hello [str my, str friend] -Hello [str this.is.a.qualified.name] -Hello -[trm - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])] -Hello -[const-decl test - (some - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] -Hello -[indt-decl - (record test (sort (typ «Set»)) Build_test - (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ - field [coercion off, canonical tt] f2 - (app - [global (indt «eq»), global (indt «nat»), c0, - app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] -The type of -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], global (indc «O»)] is -sort prop -1 = true - : Prop -T= -app - [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], - global (indc «true»)] -T1= -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], - app [global (const «bool2nat»), global (indc «true»)]] -Ty= sort prop -nK_bool = 2 - : nat -nK_False = 0 - : nat -Inductive tree' (A : Set) : Set := - leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. - -Arguments tree' A%type_scope -Arguments leaf' A%type_scope -Arguments node' A%type_scope _ _ _ -bob is 24 years old -alice is 21 years old -bob is 24 years old -alice is 21 years old -[attribute elpi.loc - (leaf-loc - File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), - attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), - attribute more (node [attribute stuff (leaf-str 33)])] -options= -[get-option elpi.loc - File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, - get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] -33 tt -That is all folks! -going from source to target via plane -synterp x := some _ -interp x := -some - (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) -The module is «elpi_examples.tutorial_coq_elpi_command.Module59» -Box.Box.Box.Box.foo = fun n : nat => n + 2 - : nat -> nat - -Arguments Box.Box.Box.Box.foo n%nat_scope -Module NextModule2 := Struct End -File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: -Warning: This command does not support this attribute: unknown. -[unsupported-attributes,parsing,default] Goal: [decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»))] |- X0 c0 c1 : @@ -3983,6 +4019,8 @@ Arguments nilR_inv A%type_scope PA%function_scope idx0%list_scope _ Arguments consR_inv A%type_scope PA%function_scope idx0%list_scope a _ xs%list_scope _ _ +Cats.And.Dogs.x = 42 + : nat File "./apps/eltac/tests/test_injection.v", line 15, characters 0-15: Warning: Using Vector.t is known to be technically difficult, see . @@ -4132,196 +4170,6 @@ Arguments pred_R (n n)%nat_scope n File "./apps/derive/tests/test_param2.v", line 85, characters 0-30: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] -Cats.And.Dogs.x = 42 - : nat -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Succ p - = false - : bool -peano_eqb_OK - : forall x1 x2 : peano, reflect (x1 = x2) (peano_eqb x1 x2) -Notation peano := peano.peano - -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments peano.Succ p -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments peano.Succ p - = false - : bool -peano.eqb_OK - : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2) -Notation peano := Peano.peano - -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Peano.Succ p -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Peano.Succ p - = false - : bool -Peano.eqb_OK - : forall x1 x2 : peano, reflect (x1 = x2) (Peano.eqb x1 x2) -Notation peano := Peano.peano - -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Peano.Succ p -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Peano.Succ p -Module -Peano -:= Struct - Inductive peano : Set := - Zero : example4.peano | Succ : example4.peano -> example4.peano. - Definition peano_rect : - forall P : example4.peano -> Type, - P example4.Zero -> - (forall p : example4.peano, P p -> P (example4.Succ p)) -> - forall p : example4.peano, P p. - Definition peano_ind : - forall P : example4.peano -> Prop, - P example4.Zero -> - (forall p : example4.peano, P p -> P (example4.Succ p)) -> - forall p : example4.peano, P p. - Definition peano_rec : - forall P : example4.peano -> Set, - P example4.Zero -> - (forall p : example4.peano, P p -> P (example4.Succ p)) -> - forall p : example4.peano, P p. - Definition peano_sind : - forall P : example4.peano -> SProp, - P example4.Zero -> - (forall p : example4.peano, P p -> P (example4.Succ p)) -> - forall p : example4.peano, P p. - Definition Peano_map : example4.peano -> example4.peano. - Inductive is_peano : example4.peano -> Type := - is_Zero : is_peano example4.Zero - | is_Succ : forall p : example4.peano, - is_peano p -> is_peano (example4.Succ p). - Definition is_peano_rect : - forall P : forall s1 : example4.peano, is_peano s1 -> Type, - P example4.Zero is_Zero -> - (forall (p : example4.peano) (Pp : is_peano p), - P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> - forall (s1 : example4.peano) (i : is_peano s1), P s1 i. - Definition is_peano_ind : - forall P : forall s1 : example4.peano, is_peano s1 -> Prop, - P example4.Zero is_Zero -> - (forall (p : example4.peano) (Pp : is_peano p), - P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> - forall (s1 : example4.peano) (i : is_peano s1), P s1 i. - Definition is_peano_rec : - forall P : forall s1 : example4.peano, is_peano s1 -> Set, - P example4.Zero is_Zero -> - (forall (p : example4.peano) (Pp : is_peano p), - P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> - forall (s1 : example4.peano) (i : is_peano s1), P s1 i. - Definition is_peano_sind : - forall P : forall s1 : example4.peano, is_peano s1 -> SProp, - P example4.Zero is_Zero -> - (forall (p : example4.peano) (Pp : is_peano p), - P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> - forall (s1 : example4.peano) (i : is_peano s1), P s1 i. - Definition reali_is_peano : reali_db example4.peano is_peano. - Definition reali_is_peano_Zero : reali_db example4.Zero is_Zero. - Definition reali_is_peano_Succ : reali_db example4.Succ is_Succ. - Inductive peano_R : example4.peano -> example4.peano -> Set := - Zero_R : peano_R example4.Zero example4.Zero - | Succ_R : forall p p0 : example4.peano, - peano_R p p0 -> - peano_R (example4.Succ p) (example4.Succ p0). - Definition peano_R_rect : - forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Type, - P example4.Zero example4.Zero Zero_R -> - (forall (p p0 : example4.peano) (p1 : peano_R p p0), - P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> - forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. - Definition peano_R_ind : - forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Prop, - P example4.Zero example4.Zero Zero_R -> - (forall (p p0 : example4.peano) (p1 : peano_R p p0), - P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> - forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. - Definition peano_R_rec : - forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Set, - P example4.Zero example4.Zero Zero_R -> - (forall (p p0 : example4.peano) (p1 : peano_R p p0), - P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> - forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. - Definition peano_R_sind : - forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> SProp, - P example4.Zero example4.Zero Zero_R -> - (forall (p p0 : example4.peano) (p1 : peano_R p p0), - P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> - forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. - Definition param_peano_R : - param_db example4.peano example4.peano peano_R. - Definition param_Zero_R : param_db example4.Zero example4.Zero Zero_R. - Definition param_Succ_R : param_db example4.Succ example4.Succ Succ_R. - Definition Peano_tag : example4.peano -> BinNums.positive. - Definition congr_is_Zero : is_Zero = is_Zero. - Definition congr_is_Succ : - forall (x : example4.peano) (p1 p2 : is_peano x), - p1 = p2 -> is_Succ x p1 = is_Succ x p2. - Definition is_peano_inhab : forall x : example4.peano, is_peano x. - Definition is_peano_functor : - forall x : example4.peano, is_peano x -> is_peano x. - Record box_peano_Zero : Type := Box_peano_Zero { }. - Record box_peano_Succ : Type := Box_peano_Succ - { Box_peano_Succ_0 : example4.peano }. - Definition Box_peano_Succ_0 : box_peano_Succ -> example4.peano. - Definition Peano_fields_t : BinNums.positive -> Type. - Definition Peano_fields : - forall i : example4.peano, Peano_fields_t (Peano_tag i). - Definition Peano_construct : - forall p : BinNums.positive, Peano_fields_t p -> option example4.peano. - Parameter Peano_constructP : - forall i : example4.peano, - Peano_construct (Peano_tag i) (Peano_fields i) = Some i. - Definition is_peano_trivial : - forall x : example4.peano, - {u : is_peano x & forall v : is_peano x, u = v}. - Definition Peano_induction : - forall P : example4.peano -> Type, - P example4.Zero -> - (forall p : example4.peano, P p -> P (example4.Succ p)) -> - forall s1 : example4.peano, is_peano s1 -> P s1. - Definition Peano_eqb_fields : - (example4.peano -> example4.peano -> bool) -> - forall x : BinNums.positive, - Peano_fields_t x -> Peano_fields_t x -> bool. - Definition Peano_eqb : example4.peano -> example4.peano -> bool. - Parameter Peano_eqb_correct : - forall x : example4.peano, eqb_correct_on Peano_eqb x. - Parameter Peano_eqb_refl : - forall x : example4.peano, eqb_refl_on Peano_eqb x. - Parameter Peano_eqb_OK : - forall x1 x2 : example4.peano, reflect (x1 = x2) (Peano_eqb x1 x2). - End - = false - : bool -Peano.Peano_eqb_OK - : forall x1 x2 : peano, reflect (x1 = x2) (Peano.Peano_eqb x1 x2) -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - -Arguments Succ p - = false - : bool -eqb_OK - : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) -Inductive peano : Set := - Zero : Peano.peano | Succ : Peano.peano -> Peano.peano. - -Arguments Peano.Succ p - = false - : bool -Peano.eqb_OK - : forall x1 x2 : Peano.peano, reflect (x1 = x2) (Peano.eqb x1 x2) Module d3 : d3_Locked @@ -4448,26 +4296,6 @@ Solution for C 1 is i1 Goal is E 1 Solution for E 1 is e1 -All the remaining goals are on the shelf. - -1 goal - -goal 1 is: - C -1 goal - - ============================ - C -All the remaining goals are on the shelf. - -1 goal - -goal 1 is: - C -1 goal - - ============================ - C Query assignments: Len = 288 Rules = [tc.instance [] (const «RelationClasses.iff_Symmetric») @@ -4960,6 +4788,33 @@ (indt «RelationClasses.PER»), tc.instance [] (const «ssrsetoid.compat_Reflexive») (const «ssrclasses.Reflexive»)] +Now click "Start watching" in the Elpi Trace Browser panel and then execute +the Command/Tactic/Query you want to trace. Also try "F1 Elpi". +(fun H : C Q => + ex_intro (fun T : Type -> Type => forall R : Type -> Type, C R -> C T) Q + (fun (R : Type -> Type) (_ : C R) => let H1 : C Q := H in H1)) +Now click "Start watching" in the Elpi Trace Browser panel and then execute +the Command/Tactic/Query you want to trace. Also try "F1 Elpi". +All the remaining goals are on the shelf. + +1 goal + +goal 1 is: + C +1 goal + + ============================ + C +All the remaining goals are on the shelf. + +1 goal + +goal 1 is: + C +1 goal + + ============================ + C File "./apps/tc/tests/test_tc.v", line 10, characters 0-19: Warning: There is an hint extern in the typeclass db: @@ -5282,13 +5137,6 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -Now click "Start watching" in the Elpi Trace Browser panel and then execute -the Command/Tactic/Query you want to trace. Also try "F1 Elpi". -(fun H : C Q => - ex_intro (fun T : Type -> Type => forall R : Type -> Type, C R -> C T) Q - (fun (R : Type -> Type) (_ : C R) => let H1 : C Q := H in H1)) -Now click "Start watching" in the Elpi Trace Browser panel and then execute -the Command/Tactic/Query you want to trace. Also try "F1 Elpi". (fun x : tele => tele_fmap) Normalizing app [global (indt «nat2»), global (indc «S»)] Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] @@ -5430,12 +5278,200 @@ forall (T : Type -> Type) (H : forall x : Type, T x), C2 T (fun x : Type => H x) -> D Debug: [tactic-unification] Leaving unification with success -ok +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Succ p + = false + : bool +peano_eqb_OK + : forall x1 x2 : peano, reflect (x1 = x2) (peano_eqb x1 x2) +Notation peano := peano.peano + +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments peano.Succ p +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments peano.Succ p + = false + : bool +peano.eqb_OK + : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2) +Notation peano := Peano.peano + +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Peano.Succ p +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Peano.Succ p + = false + : bool +Peano.eqb_OK + : forall x1 x2 : peano, reflect (x1 = x2) (Peano.eqb x1 x2) +Notation peano := Peano.peano + +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Peano.Succ p +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Peano.Succ p +Module +Peano +:= Struct + Inductive peano : Set := + Zero : example4.peano | Succ : example4.peano -> example4.peano. + Definition peano_rect : + forall P : example4.peano -> Type, + P example4.Zero -> + (forall p : example4.peano, P p -> P (example4.Succ p)) -> + forall p : example4.peano, P p. + Definition peano_ind : + forall P : example4.peano -> Prop, + P example4.Zero -> + (forall p : example4.peano, P p -> P (example4.Succ p)) -> + forall p : example4.peano, P p. + Definition peano_rec : + forall P : example4.peano -> Set, + P example4.Zero -> + (forall p : example4.peano, P p -> P (example4.Succ p)) -> + forall p : example4.peano, P p. + Definition peano_sind : + forall P : example4.peano -> SProp, + P example4.Zero -> + (forall p : example4.peano, P p -> P (example4.Succ p)) -> + forall p : example4.peano, P p. + Definition Peano_map : example4.peano -> example4.peano. + Inductive is_peano : example4.peano -> Type := + is_Zero : is_peano example4.Zero + | is_Succ : forall p : example4.peano, + is_peano p -> is_peano (example4.Succ p). + Definition is_peano_rect : + forall P : forall s1 : example4.peano, is_peano s1 -> Type, + P example4.Zero is_Zero -> + (forall (p : example4.peano) (Pp : is_peano p), + P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> + forall (s1 : example4.peano) (i : is_peano s1), P s1 i. + Definition is_peano_ind : + forall P : forall s1 : example4.peano, is_peano s1 -> Prop, + P example4.Zero is_Zero -> + (forall (p : example4.peano) (Pp : is_peano p), + P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> + forall (s1 : example4.peano) (i : is_peano s1), P s1 i. + Definition is_peano_rec : + forall P : forall s1 : example4.peano, is_peano s1 -> Set, + P example4.Zero is_Zero -> + (forall (p : example4.peano) (Pp : is_peano p), + P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> + forall (s1 : example4.peano) (i : is_peano s1), P s1 i. + Definition is_peano_sind : + forall P : forall s1 : example4.peano, is_peano s1 -> SProp, + P example4.Zero is_Zero -> + (forall (p : example4.peano) (Pp : is_peano p), + P p Pp -> P (example4.Succ p) (is_Succ p Pp)) -> + forall (s1 : example4.peano) (i : is_peano s1), P s1 i. + Definition reali_is_peano : reali_db example4.peano is_peano. + Definition reali_is_peano_Zero : reali_db example4.Zero is_Zero. + Definition reali_is_peano_Succ : reali_db example4.Succ is_Succ. + Inductive peano_R : example4.peano -> example4.peano -> Set := + Zero_R : peano_R example4.Zero example4.Zero + | Succ_R : forall p p0 : example4.peano, + peano_R p p0 -> + peano_R (example4.Succ p) (example4.Succ p0). + Definition peano_R_rect : + forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Type, + P example4.Zero example4.Zero Zero_R -> + (forall (p p0 : example4.peano) (p1 : peano_R p p0), + P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> + forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. + Definition peano_R_ind : + forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Prop, + P example4.Zero example4.Zero Zero_R -> + (forall (p p0 : example4.peano) (p1 : peano_R p p0), + P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> + forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. + Definition peano_R_rec : + forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> Set, + P example4.Zero example4.Zero Zero_R -> + (forall (p p0 : example4.peano) (p1 : peano_R p p0), + P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> + forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. + Definition peano_R_sind : + forall P : forall s1 s2 : example4.peano, peano_R s1 s2 -> SProp, + P example4.Zero example4.Zero Zero_R -> + (forall (p p0 : example4.peano) (p1 : peano_R p p0), + P p p0 p1 -> P (example4.Succ p) (example4.Succ p0) (Succ_R p p0 p1)) -> + forall (s1 s2 : example4.peano) (p : peano_R s1 s2), P s1 s2 p. + Definition param_peano_R : + param_db example4.peano example4.peano peano_R. + Definition param_Zero_R : param_db example4.Zero example4.Zero Zero_R. + Definition param_Succ_R : param_db example4.Succ example4.Succ Succ_R. + Definition Peano_tag : example4.peano -> BinNums.positive. + Definition congr_is_Zero : is_Zero = is_Zero. + Definition congr_is_Succ : + forall (x : example4.peano) (p1 p2 : is_peano x), + p1 = p2 -> is_Succ x p1 = is_Succ x p2. + Definition is_peano_inhab : forall x : example4.peano, is_peano x. + Definition is_peano_functor : + forall x : example4.peano, is_peano x -> is_peano x. + Record box_peano_Zero : Type := Box_peano_Zero { }. + Record box_peano_Succ : Type := Box_peano_Succ + { Box_peano_Succ_0 : example4.peano }. + Definition Box_peano_Succ_0 : box_peano_Succ -> example4.peano. + Definition Peano_fields_t : BinNums.positive -> Type. + Definition Peano_fields : + forall i : example4.peano, Peano_fields_t (Peano_tag i). + Definition Peano_construct : + forall p : BinNums.positive, Peano_fields_t p -> option example4.peano. + Parameter Peano_constructP : + forall i : example4.peano, + Peano_construct (Peano_tag i) (Peano_fields i) = Some i. + Definition is_peano_trivial : + forall x : example4.peano, + {u : is_peano x & forall v : is_peano x, u = v}. + Definition Peano_induction : + forall P : example4.peano -> Type, + P example4.Zero -> + (forall p : example4.peano, P p -> P (example4.Succ p)) -> + forall s1 : example4.peano, is_peano s1 -> P s1. + Definition Peano_eqb_fields : + (example4.peano -> example4.peano -> bool) -> + forall x : BinNums.positive, + Peano_fields_t x -> Peano_fields_t x -> bool. + Definition Peano_eqb : example4.peano -> example4.peano -> bool. + Parameter Peano_eqb_correct : + forall x : example4.peano, eqb_correct_on Peano_eqb x. + Parameter Peano_eqb_refl : + forall x : example4.peano, eqb_refl_on Peano_eqb x. + Parameter Peano_eqb_OK : + forall x1 x2 : example4.peano, reflect (x1 = x2) (Peano_eqb x1 x2). + End + = false + : bool +Peano.Peano_eqb_OK + : forall x1 x2 : peano, reflect (x1 = x2) (Peano.Peano_eqb x1 x2) +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + +Arguments Succ p + = false + : bool +eqb_OK + : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) +Inductive peano : Set := + Zero : Peano.peano | Succ : Peano.peano -> Peano.peano. + +Arguments Peano.Succ p + = false + : bool +Peano.eqb_OK + : forall x1 x2 : Peano.peano, reflect (x1 = x2) (Peano.eqb x1 x2) Query assignments: S = app [global (const «IsAnimal»), global (indc «Fly»), global (const «dove»)] Query assignments: S = X0 +ok File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: Warning: There is an hint extern in the typeclass db: @@ -6418,13 +6454,15 @@ (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] Debug: [elpitime] Elpi: get_and_compile 0.0000 -Debug: [TC] - Time of instance search is 0.000057 -Debug: [TC] - Time of refine.typecheck is 0.000164 +Debug: [TC] - Time of instance search is 0.000039 +Debug: [TC] - Time of refine.typecheck is 0.000122 Debug: [elpitime] - Elpi: query-compilation:0.0002 static-check:0.0000 optimization:0.0067 runtime:0.0017 (with success) + Elpi: query-compilation:0.0001 static-check:0.0000 optimization:0.0047 runtime:0.0012 (with success) -Finished transaction in 0.009 secs (0.005u,0.003s) (successful) +Finished transaction in 0.006 secs (0.006u,0.s) (successful) +Received the following event +[str new_instance, str I4, str A, str Export, int -1] File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: @@ -7069,8 +7107,6 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -Received the following event -[str new_instance, str I4, str A, str Export, int -1] File "./apps/tc/tests/importOrder/f3f.v", line 7, characters 2-23: Warning: There is an hint extern in the typeclass db: @@ -13524,13 +13560,13 @@ Skipping derivation tag on indt «nat» since it has been already run Skipping derivation eqType_ast on indt «nat» since it has been already run Derivation projK on indt «nat» -Derivation projK on indt «nat» took 0.001124 +Derivation projK on indt «nat» took 0.000809 Derivation isK on indt «nat» -Derivation isK on indt «nat» took 0.001066 +Derivation isK on indt «nat» took 0.000757 Derivation eq on indt «nat» -Derivation eq on indt «nat» took 0.001004 +Derivation eq on indt «nat» took 0.000698 Derivation invert on indt «nat» -Derivation invert on indt «nat» took 0.001080 +Derivation invert on indt «nat» took 0.000725 Skipping derivation lens_laws on indt «nat» since it has been already run Skipping derivation param1_congr on indt «nat» since it has been already run @@ -13540,7 +13576,7 @@ since it has been already run Skipping derivation fields on indt «nat» since it has been already run Derivation bcongr on indt «nat» -Derivation bcongr on indt «nat» took 0.001803 +Derivation bcongr on indt «nat» took 0.001367 Derivation idx2inv on indt «nat» Derivation idx2inv on indt «nat» failed, continuing Skipping derivation param1_trivial on indt «nat» @@ -13548,13 +13584,13 @@ Skipping derivation induction on indt «nat» since it has been already run Skipping derivation eqb on indt «nat» since it has been already run Derivation eqK on indt «nat» -Derivation eqK on indt «nat» took 0.002201 +Derivation eqK on indt «nat» took 0.001549 Skipping derivation eqbcorrect on indt «nat» since it has been already run Derivation eqcorrect on indt «nat» -Derivation eqcorrect on indt «nat» took 0.000636 +Derivation eqcorrect on indt «nat» took 0.000444 Skipping derivation eqbOK on indt «nat» since it has been already run Derivation eqOK on indt «nat» -Derivation eqOK on indt «nat» took 0.000355 +Derivation eqOK on indt «nat» took 0.000235 Skipping derivation map on indt «nat» since the user did not select it Skipping derivation lens on indt «nat» since the user did not select it Skipping derivation param1 on indt «nat» since it has been already run @@ -14036,7 +14072,7 @@ _uvk_3_ = X2 _uvk_4_ = X3 _uvk_5_ = X4 -Finished transaction in 0.087 secs (0.079u,0.007s) (successful) +Finished transaction in 0.066 secs (0.058u,0.007s) (successful) Query assignments: A = c0 \ c0 @@ -14316,8 +14352,8 @@ dpkg-gencontrol: warning: package libcoq-elpi: substitution variable ${shlibs:Depends} unused, but is defined dh_md5sums dh_builddeb -dpkg-deb: building package 'libcoq-elpi-dbgsym' in '../libcoq-elpi-dbgsym_2.2.3-1_amd64.deb'. dpkg-deb: building package 'libcoq-elpi' in '../libcoq-elpi_2.2.3-1_amd64.deb'. +dpkg-deb: building package 'libcoq-elpi-dbgsym' in '../libcoq-elpi-dbgsym_2.2.3-1_amd64.deb'. dpkg-genbuildinfo --build=binary -O../coq-elpi_2.2.3-1_amd64.buildinfo dpkg-genchanges --build=binary -O../coq-elpi_2.2.3-1_amd64.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -14325,12 +14361,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: including full source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/761097/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/3008132 and its subdirectories -I: Current time: Wed Jan 21 02:54:28 -12 2026 -I: pbuilder-time-stamp: 1769007268 +I: removing directory /srv/workspace/pbuilder/761097 and its subdirectories +I: Current time: Thu Dec 19 22:34:03 +14 2024 +I: pbuilder-time-stamp: 1734597243