--- /srv/reproducible-results/rbuild-debian/r-b-build.PZndSf9w/b1/coq-iris_4.0.0-3_i386.changes +++ /srv/reproducible-results/rbuild-debian/r-b-build.PZndSf9w/b2/coq-iris_4.0.0-3_i386.changes ├── Files │ @@ -1,2 +1,2 @@ │ │ - 0ea2244f2bc302c5a801c24703b403e0 11674248 ocaml optional libcoq-iris_4.0.0-3_i386.deb │ + f248797d27736b30b26474b3a0b45c43 11674888 ocaml optional libcoq-iris_4.0.0-3_i386.deb ├── libcoq-iris_4.0.0-3_i386.deb │ ├── file list │ │ @@ -1,3 +1,3 @@ │ │ -rw-r--r-- 0 0 0 4 2023-01-25 12:04:26.000000 debian-binary │ │ -rw-r--r-- 0 0 0 12268 2023-01-25 12:04:26.000000 control.tar.xz │ │ --rw-r--r-- 0 0 0 11661788 2023-01-25 12:04:26.000000 data.tar.xz │ │ +-rw-r--r-- 0 0 0 11662428 2023-01-25 12:04:26.000000 data.tar.xz │ ├── control.tar.xz │ │ ├── control.tar │ │ │ ├── ./control │ │ │ │ @@ -1,13 +1,13 @@ │ │ │ │ Package: libcoq-iris │ │ │ │ Source: coq-iris │ │ │ │ Version: 4.0.0-3 │ │ │ │ Architecture: i386 │ │ │ │ Maintainer: Debian OCaml Maintainers │ │ │ │ -Installed-Size: 41302 │ │ │ │ +Installed-Size: 41303 │ │ │ │ Depends: libcoq-stdpp-8tm49 │ │ │ │ Provides: libcoq-iris-dv9t7 │ │ │ │ Section: ocaml │ │ │ │ Priority: optional │ │ │ │ Homepage: https://gitlab.mpi-sws.org/iris/iris │ │ │ │ Description: high-order concurrent separation logic framework for Coq │ │ │ │ This package provides a high-order concurrent separation │ │ │ ├── ./md5sums │ │ │ │ ├── ./md5sums │ │ │ │ │┄ Files differ │ ├── data.tar.xz │ │ ├── data.tar │ │ │ ├── file list │ │ │ │ @@ -530,15 +530,15 @@ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2023-01-25 12:04:26.000000 ./usr/share/doc/libcoq-iris/ │ │ │ │ -rw-r--r-- 0 root (0) root (0) 305 2023-01-25 12:04:26.000000 ./usr/share/doc/libcoq-iris/changelog.Debian.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 29841 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/changelog.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 36859 2023-01-25 12:04:26.000000 ./usr/share/doc/libcoq-iris/copyright │ │ │ │ -rw-r--r-- 0 root (0) root (0) 7898 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/editor.md.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 3473 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/equalities_and_entailments.md.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 3438 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/heap_lang.md.gz │ │ │ │ --rw-r--r-- 0 root (0) root (0) 860965 2023-01-25 12:04:26.000000 ./usr/share/doc/libcoq-iris/iris.pdf.gz │ │ │ │ +-rw-r--r-- 0 root (0) root (0) 861603 2023-01-25 12:04:26.000000 ./usr/share/doc/libcoq-iris/iris.pdf.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 3601 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/proof_guide.md.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 8244 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/proof_mode.md.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 5453 2022-08-17 16:54:51.000000 ./usr/share/doc/libcoq-iris/resource_algebras.md.gz │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2023-01-25 12:04:26.000000 ./usr/share/doc-base/ │ │ │ │ -rw-r--r-- 0 root (0) root (0) 157 2023-01-25 12:04:26.000000 ./usr/share/doc-base/libcoq-iris.coq-iris │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2023-01-25 12:04:26.000000 ./var/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2023-01-25 12:04:26.000000 ./var/lib/ │ │ │ ├── ./usr/share/doc/libcoq-iris/iris.pdf.gz │ │ │ │ ├── iris.pdf │ │ │ │ │ ├── pdftotext {} - │ │ │ │ │ │ @@ -1,10 +1,10 @@ │ │ │ │ │ │ The Iris 3.7-dev Documentation │ │ │ │ │ │ http://plv.mpi-sws.org/iris/ │ │ │ │ │ │ -January 7, 2024 │ │ │ │ │ │ +February 8, 2025 │ │ │ │ │ │ │ │ │ │ │ │ Abstract │ │ │ │ │ │ This document describes formally the Iris program logic. Every result in this document │ │ │ │ │ │ has been fully verified in Coq. The latest versions of this document and the Coq formalization │ │ │ │ │ │ can be found in the git repository at https://gitlab.mpi-sws.org/iris/iris. For further │ │ │ │ │ │ information, visit the Iris project website at https://iris-project.org.