Diff of the two buildlogs: -- --- b1/build.log 2024-04-21 19:18:13.125397575 +0000 +++ b2/build.log 2024-04-21 19:38:42.840931138 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Apr 21 07:10:29 -12 2024 -I: pbuilder-time-stamp: 1713726629 +I: Current time: Mon Apr 22 09:18:28 +14 2024 +I: pbuilder-time-stamp: 1713727108 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -28,52 +28,84 @@ dpkg-source: info: applying fix_configure.sh.patch I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/16377/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/796/tmp/hooks/D01_modify_environment starting +debug: Running on virt64c. +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 Apr 21 19:18 /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/796/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/796/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='armhf' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 ' - DISTRIBUTION='trixie' - HOME='/root' - HOST_ARCH='armhf' + 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]="21" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='16fab954c0ec4a1f85b9f5f761205f18' - 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='16377' - PS1='# ' - PS2='> ' + INVOCATION_ID=f9ca9ae3068042ceb0dd8652449d9916 + LANG=C + LANGUAGE=it_CH:it + LC_ALL=C + MACHTYPE=arm-unknown-linux-gnueabihf + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnueabihf + 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=796 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.7i0mHQ2E/pbuilderrc_fXeJ --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.7i0mHQ2E/b1 --logfile b1/build.log coq-mtac2_1.4+8.18-1.dsc' - SUDO_GID='113' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://10.0.0.15:3142/' + 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.7i0mHQ2E/pbuilderrc_Eyhw --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.7i0mHQ2E/b2 --logfile b2/build.log coq-mtac2_1.4+8.18-1.dsc' + SUDO_GID=113 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://10.0.0.15:3142/ I: uname -a - Linux virt32a 6.1.0-20-armmp-lpae #1 SMP Debian 6.1.85-1 (2024-04-11) armv7l GNU/Linux + Linux i-capture-the-hostname 6.1.0-20-arm64 #1 SMP Debian 6.1.85-1 (2024-04-11) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Apr 21 07:14 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/16377/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Apr 21 07:13 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/796/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -189,7 +221,7 @@ Get: 64 http://deb.debian.org/debian trixie/main armhf libzarith-ocaml-dev armhf 1.13-2+b1 [101 kB] Get: 65 http://deb.debian.org/debian trixie/main armhf libcoq-core-ocaml-dev armhf 8.18.0+dfsg-1 [44.8 MB] Get: 66 http://deb.debian.org/debian trixie/main armhf libcoq-unicoq armhf 1.6-8.18-1 [78.9 kB] -Fetched 309 MB in 6s (52.5 MB/s) +Fetched 309 MB in 24s (12.7 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:armhf. (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 ... 19635 files and directories currently installed.) @@ -412,8 +444,8 @@ Setting up tzdata (2024a-1) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Apr 21 19:12:28 UTC 2024. -Universal Time is now: Sun Apr 21 19:12:28 UTC 2024. +Local time is now: Sun Apr 21 19:21:55 UTC 2024. +Universal Time is now: Sun Apr 21 19:21:55 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -476,7 +508,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-mtac2-1.4+8.18/ && 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-mtac2_1.4+8.18-1_source.changes +I: user script /srv/workspace/pbuilder/796/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/796/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-mtac2-1.4+8.18/ && 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-mtac2_1.4+8.18-1_source.changes dpkg-buildpackage: info: source package coq-mtac2 dpkg-buildpackage: info: source version 1.4+8.18-1 dpkg-buildpackage: info: source distribution unstable @@ -511,7 +547,7 @@ Warning: in orphan_Mtac2Tests_Mtac2 make[1]: Leaving directory '/build/reproducible-path/coq-mtac2-1.4+8.18' dh_auto_build - make -j3 "INSTALL=install --strip-program=true" + make -j4 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18' COQDEP VFILES COQPP src/metaCoqInit.mlg @@ -525,11 +561,11 @@ OCAMLLIBDEP src/MetaCoqPlugin.mlpack CAMLDEP src/metaCoqInterp.ml CAMLDEP src/run.ml -*** Warning: in file theories/Base.v, declared ML module ../../../usr/lib/ocaml/coq-unicoq/unicoq.cma has not been found! CAMLDEP src/mConstr.ml CAMLDEP src/mtacNames.ml CAMLDEP src/constrs.ml CAMLDEP src/metaCoqTactic.ml +*** Warning: in file theories/Base.v, declared ML module ../../../usr/lib/ocaml/coq-unicoq/unicoq.cma has not been found! CAMLDEP src/metaCoqInit.ml COQC theories/lib/Logic.v COQC theories/lib/Datatypes.v @@ -570,31 +606,31 @@ COQC theories/intf/MTele.v COQC theories/intf/Exceptions.v COQC theories/intf/Reduction.v +COQC theories/intf/Case.v File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] +COQC theories/lib/Utils.v File "./theories/intf/MTele.v", line 151, characters 0-224: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] -COQC theories/intf/Case.v -COQC theories/lib/Utils.v CAMLOPT -c -for-pack MetaCoqPlugin src/mtacNames.ml -COQC theories/Pattern.v CAMLOPT -c -for-pack MetaCoqPlugin src/mConstr.ml +COQC theories/Pattern.v CAMLOPT -c -for-pack MetaCoqPlugin src/run.ml +File "src/run.ml", line 735, characters 41-52: +735 | let coq_constr = mkConstruct constr in + ^^^^^^^^^^^ +Alert deprecated: EConstr.mkConstruct +Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct] ptele (fun x : nat => pbase true ?y UniCoq) : pattern bool ?B where ?B : [ |- bool -> Prop] ?y : [x : nat |- ?B true] COQC theories/intf/M.v -File "src/run.ml", line 735, characters 41-52: -735 | let coq_constr = mkConstruct constr in - ^^^^^^^^^^^ -Alert deprecated: EConstr.mkConstruct -Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct] File "./theories/intf/M.v", line 3, characters 0-80: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -602,7 +638,6 @@ Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInterp.ml -COQC theories/intf/Lift.v File "src/metaCoqInterp.ml", line 195, characters 36-51: 195 | ((false, sigma, ty, EConstr.mkConst c), None) ^^^^^^^^^^^^^^^ @@ -616,6 +651,7 @@ CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInit.ml CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqTactic.ml CAMLOPT -pack -o src/MetaCoqPlugin.cmx +COQC theories/intf/Lift.v CAMLOPT -a -o src/MetaCoqPlugin.cmxa CAMLOPT -shared -o src/MetaCoqPlugin.cmxs COQC theories/Base.v @@ -625,10 +661,6 @@ COQC theories/meta/MTeleMatchDef.v COQC theories/tactics/TacticsBase.v COQC theories/meta/MFixDef.v -File "./theories/meta/MTeleMatchDef.v", line 69, characters 0-12: -Warning: Use of “Require” inside a module is fragile. It is not recommended -to use this functionality in finished proof scripts. -[require-in-module,fragile,default] COQC theories/ideas/Abstract.v File "./theories/meta/MFixDef.v", line 1, characters 0-44: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. @@ -637,6 +669,10 @@ Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] COQC theories/meta/Exhaustive.v +File "./theories/meta/MTeleMatchDef.v", line 69, characters 0-12: +Warning: Use of “Require” inside a module is fragile. It is not recommended +to use this functionality in finished proof scripts. +[require-in-module,fragile,default] COQC theories/meta/MTeleMatch.v File "./theories/meta/Exhaustive.v", line 61, characters 0-165: Warning: This notation contains Ltac expressions: it will not be used for @@ -723,6 +759,7 @@ COQC theories/DecomposeApp.v COQC theories/tactics/ImportedTactics.v COQC theories/tactics/Ttactics.v +COQC theories/ideas/SubgoalsStrict.v File "./theories/DecomposeApp.v", line 1, characters 0-95: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -735,25 +772,24 @@ File "./theories/DecomposeApp.v", line 77, characters 0-173: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing,default] +File "./theories/DecomposeApp.v", line 105, characters 0-174: +Warning: This notation contains Ltac expressions: it will not be used for +printing. [non-reversible-notation,parsing,default] File "./theories/tactics/Ttactics.v", line 182, characters 0-30: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. [require-in-module,fragile,default] -COQC theories/ideas/SubgoalsStrict.v -File "./theories/DecomposeApp.v", line 105, characters 0-174: -Warning: This notation contains Ltac expressions: it will not be used for -printing. [non-reversible-notation,parsing,default] File "./theories/DecomposeApp.v", line 111, characters 0-185: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing,default] COQC theories/tactics/IntroPatt.v +COQC theories/tactics/CompoundTactics.v +COQC theories/Mtac2.v File "./theories/tactics/Ttactics.v", line 293, characters 0-20: Warning: This command is just asserting the names of arguments of gbase. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes' [arguments-assert,vernacular,default] -COQC theories/tactics/CompoundTactics.v -COQC theories/Mtac2.v COQC theories/ideas/DepDestruct.v COQC theories/tactics/ConstrSelector.v COQC theories/ideas/SumRun.v @@ -778,16 +814,11 @@ disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] COQC theories/ideas/Transport.v -Finished transaction in 0.221 secs (0.221u,0.s) (successful) +Finished transaction in 0.993 secs (0.248u,0.s) (successful) COQC tests/ConstrSelector.v COQC tests/DepDestruct.v COQC tests/Exhaustive.v -mmatch 1 with -| [# ] S | _ : nat =n> M.print "S" -| [# ] 0 | =n> M.print "O" -| _ as _ => M.print "not in constructor normal form" -end - : idmatcher_return M_InDepMatcher +COQC tests/UnivSanityCheck.v = 0 : nat = 1 @@ -804,8 +835,8 @@ ?A : [ |- Type] ?runner : [ |- M.runner (index nil)] mmatch 1 with -| [# ] 0 | =n> M.print "O" | [# ] S | _ : nat =n> M.print "S" +| [# ] 0 | =n> M.print "O" | _ as _ => M.print "not in constructor normal form" end : idmatcher_return M_InDepMatcher @@ -815,17 +846,31 @@ ?A : [ |- Type] ?runner : [ |- M.runner (index cons)] mmatch 1 with +| [# ] 0 | =n> M.print "O" +| [# ] S | _ : nat =n> M.print "S" +| _ as _ => M.print "not in constructor normal form" +end + : idmatcher_return M_InDepMatcher +Universes written to file "universes-mtac2.txt". +mmatch 1 with | _ as _ => M.print "always triggered first" | [# ] 0 | =n> M.print "O, never triggered" | [# ] S | _ : nat =n> M.print "S, never triggered" end : idmatcher_return M_InDepMatcher +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] +0 + = Z0 + : Z +[DEBUG] Running test mmatch (1 :: nil)%list with | [# ] nil | =n> M.print "nil" | [# ] cons | (_ : nat) (_ : list nat) =n> M.print "cons" | _ as _ => M.print "not in constructor normal form" end : idmatcher_return M_InDepMatcher +[OK] tests/UnivSanityCheck.v +COQC tests/abs.v mmatch (1 :: nil)%list with | [# ] nil | =n> M.print "nil" | [# ] cons | (_ : nat) (_ : list nat) =n> M.print "cons" @@ -833,7 +878,7 @@ end : idmatcher_return M_InDepMatcher [OK] tests/Exhaustive.v -COQC tests/UnivSanityCheck.v +COQC tests/abs_prod.v [DEBUG] {| case_ind := nat; case_val := 3; @@ -841,27 +886,17 @@ case_branches := [m: Dyn true | Dyn (fun _ : nat => false)] |} -Universes written to file "universes-mtac2.txt". -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] -0 - = Z0 - : Z -[DEBUG] Running test -[OK] tests/UnivSanityCheck.v -COQC tests/abs.v -[OK] tests/ConstrSelector.v -COQC tests/abs_prod.v -[OK] tests/DepDestruct.v -COQC tests/binders.v [OK] tests/abs.v -COQC tests/bug_universes.v +COQC tests/binders.v [DEBUG] (nat -> (fun T : Type => T) Type) [OK] tests/abs_prod.v +COQC tests/bug_universes.v +[OK] tests/ConstrSelector.v COQC tests/bugs.v +[OK] tests/DepDestruct.v +COQC tests/cevar.v [DEBUG] (NameExistsInContext (TheName "x")) [DEBUG] (VarAppearsInValue z) -[OK] tests/binders.v -COQC tests/cevar.v File "./tests/bug_universes.v", line 36, characters 0-111: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope pattern_scope.". @@ -870,6 +905,8 @@ Warning: Variable H does not occur in the right-hand side. The notation will not be used for printing as it is not reversible. [non-reversible-notation,parsing,default] +[OK] tests/binders.v +COQC tests/comptactics.v testMmatch@{i j} = fun x : Type@{i} => x : Type@{i} -> Type@{max(i,j)} @@ -896,23 +933,23 @@ testexact is opaque Expands to: Constant Mtac2Tests.bug_universes.testexact [OK] tests/bug_universes.v -COQC tests/comptactics.v +COQC tests/debug_ex.v [DEBUG] true [DEBUG] (Metavar Propₛ (1 = 1) ?e) [OK] tests/bugs.v -COQC tests/debug_ex.v -[OK] tests/cevar.v COQC tests/decapp.v +[OK] tests/cevar.v +COQC tests/declare.v [DEBUG] raise ?e Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. [DEBUG] (StuckTerm ?t) [OK] tests/debug_ex.v -COQC tests/declare.v +COQC tests/decompose.v [DEBUG] (Specif.msigT (MTele.MTele_Const nat)) [OK] tests/decapp.v -COQC tests/decompose.v -[OK] tests/comptactics.v COQC tests/dependent_let_goals.v +[OK] tests/comptactics.v +COQC tests/destruct_eq.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -976,11 +1013,13 @@ (@M.runner unit ev), 0 subgoal(s) = tt : unit +[OK] tests/decompose.v [DEBUG] NAT3 = tt : unit NAT4 = 4 : nat +COQC tests/do.v [DEBUG] blu = tt : unit @@ -1059,10 +1098,8 @@ (fun (_ : Type -> forall a : nat, a = a -> Type) (_ : Type) (k : nat) => (m:[m:]; tt)) : M unit -[OK] tests/decompose.v = tt : unit -COQC tests/destruct_eq.v = (MTele_val (curry_sort Typeₛ (fun a' : ArgsOf P => @@ -1204,8 +1241,6 @@ mexistT (MTele_ConstT S.Sort) [tele ] Propₛ) a))) mt_constr}) *m unit)))) -> M unit : Type -[OK] tests/dependent_let_goals.v -COQC tests/do.v = tt : unit = (MTele_val @@ -1252,6 +1287,8 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit)))) -> M unit : Type +[OK] tests/dependent_let_goals.v +COQC tests/dummylang.v = tt : unit Debug: @@ -1271,7 +1308,7 @@ Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) [OK] tests/declare.v -COQC tests/dummylang.v +COQC tests/exceptions.v If ffalse or nil then ;; else If ttrue then ;; else ;; end end : st File "./tests/dummylang.v", line 69, characters 0-70: @@ -1287,24 +1324,22 @@ : Exception [DEBUG] nat [OK] tests/do.v -COQC tests/exceptions.v -[OK] tests/destruct_eq.v COQC tests/goal_reordering.v -[OK] tests/exceptions.v +[OK] tests/destruct_eq.v COQC tests/hugo.v -[OK] tests/goal_reordering.v +[OK] tests/exceptions.v COQC tests/hyps.v -[OK] tests/hyps.v +[OK] tests/goal_reordering.v COQC tests/initialization.v [OK] tests/hugo.v COQC tests/intropatt.v -[OK] tests/initialization.v +[OK] tests/hyps.v COQC tests/kind_of_term.v -[OK] tests/dummylang.v +[OK] tests/initialization.v COQC tests/lift.v [OK] tests/kind_of_term.v -COQC tests/ltac.v [DEBUG] hola +COQC tests/ltac.v [OK] tests/lift.v COQC tests/ltac_rewrite.v File "./tests/ltac.v", line 7, characters 0-32: @@ -1312,17 +1347,15 @@ notation. [unusable-identifier,parsing,default] [OK] tests/ltac_rewrite.v COQC tests/match_goal_context.v +[OK] tests/dummylang.v +COQC tests/mctacticstests.v File "./tests/ltac.v", line 60, characters 0-32: Warning: The Ltac name injection may be unusable because of a conflict with a notation. [unusable-identifier,parsing,default] [OK] tests/ltac.v -COQC tests/mctacticstests.v -[OK] tests/intropatt.v COQC tests/min_bug_univpoly.v [OK] tests/match_goal_context.v COQC tests/min_bug_univpoly2.v -[OK] tests/min_bug_univpoly2.v -COQC tests/mode.v File "./tests/min_bug_univpoly.v", line 27, characters 0-118: Warning: Notation "_ = _ :> _" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -1338,6 +1371,10 @@ File "./tests/min_bug_univpoly.v", line 34, characters 0-47: Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing,default] +[OK] tests/min_bug_univpoly2.v +COQC tests/mode.v +[OK] tests/intropatt.v +COQC tests/mono_list_issue.v File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -1350,14 +1387,12 @@ File "./tests/min_bug_univpoly.v", line 234, characters 0-66: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing,default] -[OK] tests/mode.v -COQC tests/mono_list_issue.v -[OK] tests/min_bug_univpoly.v -COQC tests/mrun.v File "./tests/mono_list_issue.v", line 3, characters 0-29: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. [require-in-module,fragile,default] +[OK] tests/min_bug_univpoly.v +COQC tests/mrun.v File "./tests/mono_list_issue.v", line 26, characters 0-67: Warning: Notation "_ :: _" was already used in scope list_scope. [notation-overridden,parsing,default] @@ -1366,67 +1401,77 @@ [notation-overridden,parsing,default] [OK] tests/mono_list_issue.v COQC tests/names.v -[OK] tests/mrun.v +[OK] tests/mode.v COQC tests/nu_let.v [OK] tests/names.v COQC tests/pretype.v [OK] tests/nu_let.v COQC tests/reduction.v -[OK] tests/pretype.v +[OK] tests/mrun.v COQC tests/reif_jason.v +[OK] tests/pretype.v +COQC tests/removetest.v is_not_breaking_letins = id I : True -Finished transaction in 0.709 secs (0.516u,0.051s) (successful) -Finished transaction in 0.146 secs (0.074u,0.s) (successful) -[DEBUG] b -[DEBUG] nat -[OK] tests/reduction.v -COQC tests/removetest.v -[DEBUG] b -[DEBUG] nat -[DEBUG] b -[DEBUG] nat +Finished transaction in 3.474 secs (0.704u,0.052s) (successful) File "./tests/reif_jason.v", line 596, characters 2-322: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] +Finished transaction in 0.321 secs (0.071u,0.003s) (successful) [OK] tests/reif_jason.v COQC tests/replace.v -(fun H : if true then True else False => H) -[OK] tests/replace.v +[OK] tests/reduction.v COQC tests/rew_hd_error.v +[DEBUG] b +[DEBUG] nat +[DEBUG] b +[DEBUG] nat [OK] tests/removetest.v COQC tests/selectors.v -[OK] tests/rew_hd_error.v +[DEBUG] b +(fun H : if true then True else False => H) +[DEBUG] nat +[OK] tests/replace.v COQC tests/ssrpattern.v -(fun (x : nat) (z : bool) (y : nat) => ?Goal z y x) +[OK] tests/rew_hd_error.v +COQC tests/tactics.v [DEBUG] (fun n : nat => n + n = S (S (S n))) [DEBUG] (fun n : nat => ?n + n = S (S (S n))) [OK] tests/ssrpattern.v -COQC tests/tactics.v -[OK] tests/selectors.v COQC tests/test_bind.v -[OK] tests/test_bind.v +[OK] tests/selectors.v COQC tests/test_brackets.v -[OK] tests/mctacticstests.v +[OK] tests/test_bind.v COQC tests/test_get_name.v +(fun (x : nat) (z : bool) (y : nat) => ?Goal z y x) [OK] tests/test_get_name.v COQC tests/test_get_reference.v [OK] tests/test_get_reference.v COQC tests/test_goal_match.v [OK] tests/test_brackets.v COQC tests/test_mmatch.v -[OK] tests/tactics.v +[OK] tests/mctacticstests.v COQC tests/test_mtry.v -Finished transaction in 0.188 secs (0.176u,0.011s) (successful) -[OK] tests/test_goal_match.v +[OK] tests/test_mtry.v COQC tests/test_munify.v -[OK] tests/test_mmatch.v +Finished transaction in 1.019 secs (0.194u,0.043s) (successful) +[OK] tests/test_goal_match.v COQC tests/test_ret.v -[OK] tests/test_munify.v +[OK] tests/tactics.v COQC tests/test_unfold_in.v -[OK] tests/test_mtry.v -[OK] tests/test_ret.v +[OK] tests/test_munify.v COQC tests/timers.v +[OK] tests/test_ret.v COQC tests/trace.v +[OK] tests/test_unfold_in.v +COQC tests/ttactics.v +[OK] tests/test_mmatch.v +COQC tests/typeclass.v +0.274000 +0.274000 +0.532000 +0.000000 +[OK] tests/timers.v +COQC tests/typed_term_decomposition.v [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -1439,15 +1484,9 @@ [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) [OK] tests/trace.v -COQC tests/ttactics.v -[OK] tests/test_unfold_in.v -COQC tests/typeclass.v -0.058000 -0.058000 -0.109000 -0.000000 -[OK] tests/timers.v -COQC tests/typed_term_decomposition.v +COQC tests/unification.v +[OK] tests/typeclass.v +COQC tests/bugs/abs_prod_unsoundness.v (3, 5) : nat * nat 5 @@ -1455,33 +1494,42 @@ (True, False) : Prop * Prop [DEBUG] (3, 5) -[OK] tests/typeclass.v -COQC tests/unification.v [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [OK] tests/typed_term_decomposition.v -COQC tests/bugs/abs_prod_unsoundness.v -[OK] tests/ttactics.v COQC tests/bugs/bug117.v [OK] tests/unification.v COQC tests/bugs/bug225.v -[OK] tests/bugs/abs_prod_unsoundness.v +[OK] tests/ttactics.v COQC tests/bugs/bug288.v -[OK] tests/bugs/bug117.v +[OK] tests/bugs/abs_prod_unsoundness.v COQC tests/bugs/bug295.v [OK] tests/bugs/bug225.v COQC tests/bugs/bug297.v -[OK] tests/bugs/bug288.v +[OK] tests/bugs/bug117.v COQC tests/bugs/bug299.v -[OK] tests/bugs/bug297.v +[OK] tests/bugs/bug288.v COQC tests/bugs/bug302.v [OK] tests/bugs/bug295.v COQC tests/bugs/bug304.v +[OK] tests/bugs/bug297.v +COQC examples/basics_tutorial.v [DEBUG] All good, a was instantiated with b's type (tFalse) [OK] tests/bugs/bug299.v -COQC examples/basics_tutorial.v +COQC examples/tactics.v +[DEBUG] all good +[OK] tests/bugs/bug302.v +COQC examples/tauto.v +[DEBUG] All good +[OK] tests/bugs/bug304.v +cd tests/sf-5; ./configure.sh; make clean; make +Warning: No common logical root. +Warning: In this case the -docroot option should be given. +Warning: Otherwise the install-doc target is going to install files +Warning: in orphan_lf_Mtac2 +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. produces_a_value : M nat the_value_tactic = 1 @@ -1489,18 +1537,17 @@ File "./examples/basics_tutorial.v", line 97, characters 0-47: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing,default] -[DEBUG] All good -[OK] tests/bugs/bug304.v -COQC examples/tactics.v empty_string = "" : string world_string = "world" : string other_string = "other" : string +CLEAN the_sequence_6 = 6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil : list nat +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. inlist : forall (A : Type) (x : A) (x0 : list A), M (In x x0) y_in_zyx = @@ -1508,6 +1555,7 @@ : forall x y z : nat, In y (z :: y :: x :: nil) Arguments y_in_zyx (x y z)%nat_scope +COQDEP VFILES inlist' = fun (A : Type) (x : A) => mfix1 f s : list A : M In x s := @@ -1549,8 +1597,7 @@ : forall (A : Type) (x : A) (l r : list A), In x r -> In x (l ++ r) Arguments inlist'_obligation_2 [A]%type_scope x (l r)%list_scope ir -[DEBUG] all good -[OK] tests/bugs/bug302.v +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. ex_inlist = fun x y z : nat => in_cons y x @@ -1568,7 +1615,6 @@ : forall x y z : nat, In x ((y :: z :: nil) ++ x :: z :: nil) Arguments ex_inlist (x y z)%nat_scope -COQC examples/tauto.v ex_inlist' = fun x y z : nat => (fun (A : Type) (x0 : A) (_ : forall x1 : list A, M (In x0 x1)) @@ -1612,6 +1658,7 @@ Arguments ex_inlist'' (x y z)%nat_scope ex1 = conj I (or_intror I) : True /\ (False \/ True) +COQC lf/Preface.v nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B nu is universe polymorphic @@ -1623,24 +1670,9 @@ : forall p q : Prop, p -> q -> p /\ q Arguments ex_with_implication [p q]%type_scope _ _ +COQC lf/Basics.v [OK] examples/basics_tutorial.v -cd tests/sf-5; ./configure.sh; make clean; make -Warning: No common logical root. -Warning: In this case the -docroot option should be given. -Warning: Otherwise the install-doc target is going to install files -Warning: in orphan_lf_Mtac2 -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -CLEAN -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQDEP VFILES -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQC lf/Preface.v [OK] examples/tauto.v -COQC lf/Basics.v -File "./examples/tactics.v", line 208, characters 0-55: -Warning: This notation contains Ltac expressions: it will not be used for -printing. [non-reversible-notation,parsing,default] -[OK] examples/tactics.v File "./lf/Basics.v", line 15, characters 0-38: Warning: There is no flag or option with this name: "Global Default Proof Using". [unknown-option,default] @@ -1668,6 +1700,10 @@ : nat 0 + 1 + 1 : nat +File "./examples/tactics.v", line 208, characters 0-55: +Warning: This notation contains Ltac expressions: it will not be used for +printing. [non-reversible-notation,parsing,default] +[OK] examples/tactics.v COQC lf/Induction.v leb : nat -> nat -> bool @@ -1744,27 +1780,33 @@ (_ : forall x : X, @eq Y (f x) (g x)), @eq (forall _ : X, Y) f g make[1]: Leaving directory '/build/reproducible-path/coq-mtac2-1.4+8.18' dh_auto_test - make -j3 test + make -j4 test make[1]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18' COQC tests/ConstrSelector.v COQC tests/DepDestruct.v COQC tests/Exhaustive.v +COQC tests/UnivSanityCheck.v = 0 : nat + = 1 + : nat mmatch 1 with | [# ] S | _ : nat =n> M.print "S" | [# ] 0 | =n> M.print "O" | _ as _ => M.print "not in constructor normal form" end : idmatcher_return M_InDepMatcher - = 1 - : nat = let (eval) := ?runner in eval : nat where ?A : [ |- Type] ?x : [ |- ?A] ?runner : [ |- M.runner (index eq_refl)] + = let (eval) := ?runner in eval + : nat +where +?A : [ |- Type] +?runner : [ |- M.runner (index nil)] mmatch 1 with | [# ] 0 | =n> M.print "O" | [# ] S | _ : nat =n> M.print "S" @@ -1775,18 +1817,21 @@ : nat where ?A : [ |- Type] -?runner : [ |- M.runner (index nil)] - = let (eval) := ?runner in eval - : nat -where -?A : [ |- Type] ?runner : [ |- M.runner (index cons)] +Universes written to file "universes-mtac2.txt". +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] mmatch 1 with | _ as _ => M.print "always triggered first" | [# ] 0 | =n> M.print "O, never triggered" | [# ] S | _ : nat =n> M.print "S, never triggered" end : idmatcher_return M_InDepMatcher +0 + = Z0 + : Z +[DEBUG] Running test +[OK] tests/UnivSanityCheck.v +COQC tests/abs.v mmatch (1 :: nil)%list with | [# ] nil | =n> M.print "nil" | [# ] cons | (_ : nat) (_ : list nat) =n> M.print "cons" @@ -1800,7 +1845,7 @@ end : idmatcher_return M_InDepMatcher [OK] tests/Exhaustive.v -COQC tests/UnivSanityCheck.v +COQC tests/abs_prod.v [DEBUG] {| case_ind := nat; case_val := 3; @@ -1808,29 +1853,17 @@ case_branches := [m: Dyn true | Dyn (fun _ : nat => false)] |} -Universes written to file "universes-mtac2.txt". -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] -0 - = Z0 - : Z -[DEBUG] Running test -[OK] tests/UnivSanityCheck.v -COQC tests/abs.v -[OK] tests/ConstrSelector.v -COQC tests/abs_prod.v -[OK] tests/DepDestruct.v -COQC tests/binders.v [OK] tests/abs.v -COQC tests/bug_universes.v +COQC tests/binders.v [DEBUG] (nat -> (fun T : Type => T) Type) [OK] tests/abs_prod.v +COQC tests/bug_universes.v +[OK] tests/ConstrSelector.v COQC tests/bugs.v +[OK] tests/DepDestruct.v +COQC tests/cevar.v [DEBUG] (NameExistsInContext (TheName "x")) [DEBUG] (VarAppearsInValue z) -[OK] tests/binders.v -COQC tests/cevar.v -[DEBUG] true -[DEBUG] (Metavar Propₛ (1 = 1) ?e) File "./tests/bug_universes.v", line 36, characters 0-111: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope pattern_scope.". @@ -1839,8 +1872,6 @@ Warning: Variable H does not occur in the right-hand side. The notation will not be used for printing as it is not reversible. [non-reversible-notation,parsing,default] -[OK] tests/bugs.v -COQC tests/comptactics.v testMmatch@{i j} = fun x : Type@{i} => x : Type@{i} -> Type@{max(i,j)} @@ -1866,19 +1897,23 @@ Arguments testexact _%type_scope testexact is opaque Expands to: Constant Mtac2Tests.bug_universes.testexact +[OK] tests/binders.v +COQC tests/comptactics.v [OK] tests/bug_universes.v COQC tests/debug_ex.v -[OK] tests/cevar.v +[DEBUG] true +[DEBUG] (Metavar Propₛ (1 = 1) ?e) +[OK] tests/bugs.v COQC tests/decapp.v +[OK] tests/cevar.v +COQC tests/declare.v [DEBUG] raise ?e Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. [DEBUG] (StuckTerm ?t) [OK] tests/debug_ex.v -COQC tests/declare.v -[OK] tests/comptactics.v -[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) COQC tests/decompose.v -[OK] tests/decapp.v +[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) +[OK] tests/comptactics.v COQC tests/dependent_let_goals.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. @@ -1886,7 +1921,9 @@ File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing,default] +[OK] tests/decapp.v [DEBUG] bla +COQC tests/destruct_eq.v [DEBUG] bla = tt : unit @@ -1930,6 +1967,8 @@ : nat NAT3 = 3 : nat +[OK] tests/decompose.v +COQC tests/do.v NAT3: nat NAT2: nat NAT1: nat @@ -2215,6 +2254,8 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit)))) -> M unit : Type +[OK] tests/dependent_let_goals.v +COQC tests/dummylang.v = tt : unit Debug: @@ -2233,12 +2274,14 @@ Calling typeclass resolution with flags: depth = ∞,unique = false,fail = false Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) +[DEBUG] tt +Pum + : Exception +[DEBUG] nat [OK] tests/declare.v -COQC tests/destruct_eq.v -[OK] tests/dependent_let_goals.v -COQC tests/do.v -[OK] tests/decompose.v -COQC tests/dummylang.v +COQC tests/exceptions.v +[OK] tests/do.v +COQC tests/goal_reordering.v If ffalse or nil then ;; else If ttrue then ;; else ;; end end : st File "./tests/dummylang.v", line 69, characters 0-70: @@ -2249,42 +2292,34 @@ Warning: "intros until 0" is deprecated, use "intros *"; instead of "induction 0" and "destruct 0" use explicitly a name." [deprecated-intros-until-0,tactics,default] -[DEBUG] tt -Pum - : Exception -[DEBUG] nat -[OK] tests/do.v -COQC tests/exceptions.v [OK] tests/destruct_eq.v -COQC tests/goal_reordering.v -[OK] tests/exceptions.v COQC tests/hugo.v [OK] tests/goal_reordering.v COQC tests/hyps.v -[OK] tests/hyps.v +[OK] tests/exceptions.v COQC tests/initialization.v [OK] tests/hugo.v COQC tests/intropatt.v -[OK] tests/dummylang.v +[OK] tests/hyps.v COQC tests/kind_of_term.v [OK] tests/initialization.v COQC tests/lift.v [OK] tests/kind_of_term.v -COQC tests/ltac.v [DEBUG] hola +COQC tests/ltac.v [OK] tests/lift.v COQC tests/ltac_rewrite.v File "./tests/ltac.v", line 7, characters 0-32: Warning: The Ltac name induction may be unusable because of a conflict with a notation. [unusable-identifier,parsing,default] +[OK] tests/dummylang.v +COQC tests/match_goal_context.v +[OK] tests/ltac_rewrite.v +COQC tests/mctacticstests.v File "./tests/ltac.v", line 60, characters 0-32: Warning: The Ltac name injection may be unusable because of a conflict with a notation. [unusable-identifier,parsing,default] -[OK] tests/ltac_rewrite.v -COQC tests/match_goal_context.v [OK] tests/ltac.v -COQC tests/mctacticstests.v -[OK] tests/intropatt.v COQC tests/min_bug_univpoly.v [OK] tests/match_goal_context.v COQC tests/min_bug_univpoly2.v @@ -2305,6 +2340,8 @@ File "./tests/min_bug_univpoly.v", line 34, characters 0-47: Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing,default] +[OK] tests/intropatt.v +COQC tests/mono_list_issue.v File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing,default] @@ -2317,10 +2354,6 @@ File "./tests/min_bug_univpoly.v", line 234, characters 0-66: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing,default] -[OK] tests/min_bug_univpoly.v -COQC tests/mono_list_issue.v -[OK] tests/mode.v -COQC tests/mrun.v File "./tests/mono_list_issue.v", line 3, characters 0-29: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. @@ -2332,70 +2365,74 @@ Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing,default] [OK] tests/mono_list_issue.v +COQC tests/mrun.v +[OK] tests/min_bug_univpoly.v COQC tests/names.v -[OK] tests/mrun.v +[OK] tests/mode.v COQC tests/nu_let.v [OK] tests/names.v COQC tests/pretype.v [OK] tests/nu_let.v COQC tests/reduction.v -[OK] tests/pretype.v +[OK] tests/mrun.v COQC tests/reif_jason.v +[OK] tests/pretype.v +COQC tests/removetest.v is_not_breaking_letins = id I : True -[DEBUG] b -[DEBUG] nat -[DEBUG] b -[DEBUG] nat -Finished transaction in 0.753 secs (0.512u,0.047s) (successful) -[DEBUG] b -[DEBUG] nat -Finished transaction in 0.131 secs (0.079u,0.s) (successful) -[OK] tests/reduction.v -COQC tests/removetest.v +Finished transaction in 3.577 secs (0.734u,0.075s) (successful) +Finished transaction in 0.358 secs (0.078u,0.s) (successful) File "./tests/reif_jason.v", line 596, characters 2-322: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] -[OK] tests/reif_jason.v +[OK] tests/reduction.v COQC tests/replace.v -(fun H : if true then True else False => H) -[OK] tests/replace.v +[OK] tests/reif_jason.v COQC tests/rew_hd_error.v -(fun (x : nat) (z : bool) (y : nat) => ?Goal z y x) +[DEBUG] b +[DEBUG] nat [OK] tests/removetest.v -[OK] tests/rew_hd_error.v COQC tests/selectors.v +[DEBUG] b +[DEBUG] nat +(fun H : if true then True else False => H) +[OK] tests/replace.v COQC tests/ssrpattern.v +[OK] tests/rew_hd_error.v +COQC tests/tactics.v +[DEBUG] b +[DEBUG] nat [DEBUG] (fun n : nat => n + n = S (S (S n))) [DEBUG] (fun n : nat => ?n + n = S (S (S n))) [OK] tests/ssrpattern.v -COQC tests/tactics.v -[OK] tests/mctacticstests.v COQC tests/test_bind.v [OK] tests/selectors.v COQC tests/test_brackets.v [OK] tests/test_bind.v COQC tests/test_get_name.v +(fun (x : nat) (z : bool) (y : nat) => ?Goal z y x) [OK] tests/test_get_name.v COQC tests/test_get_reference.v [OK] tests/test_brackets.v COQC tests/test_goal_match.v [OK] tests/test_get_reference.v COQC tests/test_mmatch.v -[OK] tests/test_goal_match.v +[OK] tests/mctacticstests.v COQC tests/test_mtry.v -Finished transaction in 0.275 secs (0.182u,0.015s) (successful) -[OK] tests/tactics.v +Finished transaction in 0.854 secs (0.225u,0.015s) (successful) [OK] tests/test_mtry.v +[OK] tests/tactics.v COQC tests/test_munify.v COQC tests/test_ret.v -[OK] tests/test_mmatch.v +[OK] tests/test_goal_match.v COQC tests/test_unfold_in.v [OK] tests/test_ret.v COQC tests/timers.v [OK] tests/test_munify.v COQC tests/trace.v -[OK] tests/test_unfold_in.v +[OK] tests/test_mmatch.v COQC tests/ttactics.v +[OK] tests/test_unfold_in.v +COQC tests/typeclass.v [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -2408,19 +2445,19 @@ [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) [OK] tests/trace.v -COQC tests/typeclass.v -0.102000 -0.102000 -0.168000 +COQC tests/typed_term_decomposition.v +0.253000 +0.253000 +0.522000 0.000000 [OK] tests/timers.v -COQC tests/typed_term_decomposition.v -[OK] tests/ttactics.v COQC tests/unification.v [OK] tests/typeclass.v COQC tests/bugs/abs_prod_unsoundness.v (3, 5) : nat * nat +[OK] tests/ttactics.v +COQC tests/bugs/bug117.v 5 : nat (True, False) @@ -2431,30 +2468,37 @@ [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [OK] tests/typed_term_decomposition.v -COQC tests/bugs/bug117.v -[OK] tests/unification.v COQC tests/bugs/bug225.v -[OK] tests/bugs/abs_prod_unsoundness.v +[OK] tests/unification.v COQC tests/bugs/bug288.v -[OK] tests/bugs/bug117.v +[OK] tests/bugs/abs_prod_unsoundness.v COQC tests/bugs/bug295.v -[OK] tests/bugs/bug225.v +[OK] tests/bugs/bug117.v COQC tests/bugs/bug297.v -[OK] tests/bugs/bug288.v +[OK] tests/bugs/bug225.v COQC tests/bugs/bug299.v -[OK] tests/bugs/bug295.v +[OK] tests/bugs/bug288.v COQC tests/bugs/bug302.v -[OK] tests/bugs/bug297.v +[OK] tests/bugs/bug295.v COQC tests/bugs/bug304.v +[OK] tests/bugs/bug297.v +COQC examples/basics_tutorial.v [DEBUG] All good, a was instantiated with b's type (tFalse) [OK] tests/bugs/bug299.v -COQC examples/basics_tutorial.v +COQC examples/tactics.v [DEBUG] All good [OK] tests/bugs/bug304.v -COQC examples/tactics.v [DEBUG] all good -[OK] tests/bugs/bug302.v COQC examples/tauto.v +[OK] tests/bugs/bug302.v +cd tests/sf-5; ./configure.sh; make clean; make +Warning: No common logical root. +Warning: In this case the -docroot option should be given. +Warning: Otherwise the install-doc target is going to install files +Warning: in orphan_lf_Mtac2 +make[2]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +CLEAN produces_a_value : M nat the_value_tactic = 1 @@ -2462,6 +2506,9 @@ File "./examples/basics_tutorial.v", line 97, characters 0-47: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing,default] +make[2]: Leaving directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' +make[2]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. empty_string = "" : string world_string = "world" @@ -2471,6 +2518,7 @@ the_sequence_6 = 6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil : list nat +COQDEP VFILES inlist : forall (A : Type) (x : A) (x0 : list A), M (In x x0) y_in_zyx = @@ -2478,6 +2526,7 @@ : forall x y z : nat, In y (z :: y :: x :: nil) Arguments y_in_zyx (x y z)%nat_scope +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. inlist' = fun (A : Type) (x : A) => mfix1 f s : list A : M In x s := @@ -2519,6 +2568,7 @@ : forall (A : Type) (x : A) (l r : list A), In x r -> In x (l ++ r) Arguments inlist'_obligation_2 [A]%type_scope x (l r)%list_scope ir +COQC lf/Preface.v ex_inlist = fun x y z : nat => in_cons y x @@ -2579,6 +2629,7 @@ Arguments ex_inlist'' (x y z)%nat_scope ex1 = conj I (or_intror I) : True /\ (False \/ True) +COQC lf/Basics.v nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B nu is universe polymorphic @@ -2590,27 +2641,8 @@ : forall p q : Prop, p -> q -> p /\ q Arguments ex_with_implication [p q]%type_scope _ _ -[OK] examples/basics_tutorial.v -cd tests/sf-5; ./configure.sh; make clean; make -Warning: No common logical root. -Warning: In this case the -docroot option should be given. -Warning: Otherwise the install-doc target is going to install files -Warning: in orphan_lf_Mtac2 -make[2]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. [OK] examples/tauto.v -CLEAN -make[2]: Leaving directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' -make[2]: Entering directory '/build/reproducible-path/coq-mtac2-1.4+8.18/tests/sf-5' -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQDEP VFILES -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQC lf/Preface.v -COQC lf/Basics.v -File "./examples/tactics.v", line 208, characters 0-55: -Warning: This notation contains Ltac expressions: it will not be used for -printing. [non-reversible-notation,parsing,default] -[OK] examples/tactics.v +[OK] examples/basics_tutorial.v File "./lf/Basics.v", line 15, characters 0-38: Warning: There is no flag or option with this name: "Global Default Proof Using". [unknown-option,default] @@ -2638,6 +2670,10 @@ : nat 0 + 1 + 1 : nat +File "./examples/tactics.v", line 208, characters 0-55: +Warning: This notation contains Ltac expressions: it will not be used for +printing. [non-reversible-notation,parsing,default] +[OK] examples/tactics.v COQC lf/Induction.v leb : nat -> nat -> bool @@ -2883,12 +2919,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/796/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/796/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/16377 and its subdirectories -I: Current time: Sun Apr 21 07:18:08 -12 2024 -I: pbuilder-time-stamp: 1713727088 +I: removing directory /srv/workspace/pbuilder/796 and its subdirectories +I: Current time: Mon Apr 22 09:38:38 +14 2024 +I: pbuilder-time-stamp: 1713728318