OpenBSD Mail Box: August 2019

Saturday, August 31, 2019

Re: [new] xe-0.11

Brian Callahan <callab5@rpi.edu> wrote:
> I notice there's no maintainer. Evan, would you like to be maintainer
> since you've submitted this?

Attaching Brian's tarball with yours truly as maintainer. Builds,
installs, passes tests, and works for me on amd64.

Evan

sparc64 bulk build report

Re: [UPDATE] geo/gpsbabel 1.4.4 -> 1.6.0

Hello Kirill,

To build documents of GPSBabel, we have to renew docbook and docbook-xml
to use Smarty template (I don't know what the template do).
So, I think there is no better idea than your "disable building docs" now.

Here is renewed diff, (alomst the same yours and) bumped up to
GPSbabel-1.6.0.1.

diff -uNpr gpsbabel/Makefile gpsbabel.new/Makefile
--- gpsbabel/Makefile Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/Makefile Sun Sep 1 07:17:55 2019
@@ -1,81 +1,76 @@
-# $OpenBSD: Makefile,v 1.33 2018/10/24 14:28:04 sthen Exp $
+# $OpenBSD: Makefile,v 1.34 2019/07/12 20:46:29 sthen Exp $

COMMENT-main= GPS waypoint, track, and route conversion tool
COMMENT-tk= Tk front-end to gpsbabel
COMMENT-qt= Qt front-end to gpsbabel

-VERSION= 1.4.4
-DISTNAME= gpsbabel-${VERSION}
+VERSION= 1.6.0.1
+DISTNAME= gpsbabel_1_6_0.1
PKGNAME-main= gpsbabel-${VERSION}
PKGNAME-tk= gpsbabel-tk-${VERSION}
PKGNAME-qt= gpsbabel-qt-${VERSION}
CATEGORIES= geo

-REVISION-main= 2
-REVISION-tk= 2
-REVISION-qt= 3
+REVISION-main=
+REVISION-tk=
+REVISION-qt=

-HOMEPAGE= http://www.gpsbabel.org/
+HOMEPAGE= https://www.gpsbabel.org/

# GPLv2
-PERMIT_PACKAGE_CDROM= Yes
+PERMIT_PACKAGE= Yes

-MASTER_SITES= http://www.linklevel.net/distfiles/
+MASTER_SITES= https://github.com/gpsbabel/gpsbabel/archive/

COMPILER = base-clang ports-gcc base-gcc

-AUTOCONF_VERSION= 2.61
+AUTOCONF_VERSION= 2.69
CONFIGURE_STYLE= autoconf qmake
-CONFIGURE_ARGS+= --with-zlib=system \
- --with-shapefile=system \
- --with-doc=./babelweb
-#CONFIGURE_ENV+= CPPFLAGS="-I${X11BASE}/include -I${LOCALBASE}/include" \
-# LDFLAGS="-L${X11BASE}/lib -L${LOCALBASE}/lib" \
-# WEB=${WRKSRC}
+USE_GMAKE= yes
+CONFIGURE_ARGS+= --with-zlib=system
CONFIGURE_ENV+= CPPFLAGS="-I${LOCALBASE}/include" \
- LDFLAGS="-L${LOCALBASE}/lib" \
+ LDFLAGS="-L${LOCALBASE}/lib -lshp" \
WEB=${WRKSRC}

MULTI_PACKAGES= -main -tk -qt

-MODULES= devel/qmake x11/tk x11/qt4
+MODULES= devel/qmake x11/tk x11/qt5
MODQMAKE_PROJECTS = gui/app.pro
-SEPARATE_BUILD= No

-BUILD_DEPENDS= textproc/docbook-xsl
+BUILD_DEPENDS=
LIB_DEPENDS-main= devel/libusb-compat \
devel/shapelib

cWANTLIB = c m pthread
-WANTLIB-main += expat shp>=1 usb z ${cWANTLIB}
+WANTLIB-main += shp>=1 usb z ${cWANTLIB} ${COMPILER_LIBCXX}
WANTLIB-tk =
-WANTLIB-qt += ICE QtCore QtGui QtNetwork QtWebKit QtXml SM X11 Xext Xi
-WANTLIB-qt += Xinerama Xrender fontconfig freetype ${COMPILER_LIBCXX} ${cWANTLIB}
+WANTLIB-qt += GL Qt5Core Qt5Gui Qt5Network Qt5WebKit Qt5WebKitWidgets
+WANTLIB-qt += Qt5Widgets Qt5Xml ${COMPILER_LIBCXX} ${cWANTLIB}

LIB_DEPENDS-tk=
+LIB_DEPENDS-qt= x11/qt5/qtwebkit
PKG_ARCH-tk= *
RUN_DEPENDS-tk= geo/gpsbabel \
${MODTK_RUN_DEPENDS}
RUN_DEPENDS-qt= geo/gpsbabel \
devel/desktop-file-utils

+WRKDIST= ${WRKDIR}/gpsbabel-${DISTNAME}
+
pre-configure:
${SUBST_CMD} ${WRKSRC}/guibabel
@perl -pi -e 's/gpsbabelfe-bin/guibabel-qt/' \
${WRKSRC}/gui/gpsbabel.desktop

post-build:
- cd ${WRKBUILD} && make doc
${MODQMAKE_build}

do-install:
${INSTALL_PROGRAM} ${WRKBUILD}/gpsbabel ${PREFIX}/bin
- ${INSTALL_PROGRAM} ${WRKBUILD}/gui/objects/gpsbabelfe-bin \
+ ${INSTALL_PROGRAM} ${WRKBUILD}/gui/objects/gpsbabelfe \
${PREFIX}/bin/guibabel-qt
${INSTALL_SCRIPT} ${WRKSRC}/guibabel ${PREFIX}/bin
${INSTALL_DATA_DIR} ${PREFIX}/share/doc/gpsbabel
- ${INSTALL_DATA} ${WRKSRC}/babelweb/htmldoc-*/*.html \
- ${PREFIX}/share/doc/gpsbabel
${INSTALL_DATA} ${WRKSRC}/README* ${PREFIX}/share/doc/gpsbabel
${INSTALL_DATA_DIR} ${PREFIX}/share/applications
${INSTALL_DATA} ${WRKSRC}/gui/gpsbabel.desktop \
diff -uNpr gpsbabel/distinfo gpsbabel.new/distinfo
--- gpsbabel/distinfo Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/distinfo Sun Sep 1 07:17:55 2019
@@ -1,2 +1,2 @@
-SHA256 (gpsbabel-1.4.4.tar.gz) = ndKgboh8sobJoHFkqPLt4RrtEUfmQZAHNwxShBIyGUQ=
-SIZE (gpsbabel-1.4.4.tar.gz) = 7811264
+SHA256 (gpsbabel_1_6_0.1.tar.gz) = /vHVYr3ylrasXqG8ChxG+YnVU1Ro4arfEwNdU4PHTso=
+SIZE (gpsbabel_1_6_0.1.tar.gz) = 14099101
diff -uNpr gpsbabel/patches/patch-Makefile_in gpsbabel.new/patches/patch-Makefile_in
--- gpsbabel/patches/patch-Makefile_in Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/patches/patch-Makefile_in Sun Sep 1 07:17:55 2019
@@ -1,24 +1,17 @@
-$OpenBSD: patch-Makefile_in,v 1.6 2012/02/18 22:04:07 sthen Exp $
---- Makefile.in.orig Sun Jan 8 01:11:51 2012
-+++ Makefile.in Sun Jan 8 01:15:47 2012
-@@ -98,7 +98,7 @@ LIBOBJS = queue.o route.o waypt.o filter_vecs.o util.o
- uuid.o formspec.o xmltag.o cet.o cet_util.o fatal.o rgbcolors.o \
- inifile.o garmin_fs.o gbsleep.o units.o @GBSER@ gbser.o \
- gbfile.o parse.o avltree.o session.o \
-- $(PALM_DB) $(GARMIN) $(JEEPS) $(SHAPE) @ZLIB@ $(FMTS) $(FILTERS)
-+ $(PALM_DB) $(GARMIN) $(JEEPS) @SHAPE@ @ZLIB@ $(FMTS) $(FILTERS)
- OBJS = main.o globals.o $(LIBOBJS) @FILEINFO@
-
- .c.o:
-@@ -193,7 +193,6 @@ dep:
+--- Makefile.in.orig Thu May 2 17:26:47 2019
++++ Makefile.in Sat Aug 24 20:55:22 2019
+@@ -236,9 +236,8 @@ dep:
$(WEB)/htmldoc-$(DOCVERSION)/index.html: FORCE
mkdir -p $(WEB)/htmldoc-$(DOCVERSION)
perl xmldoc/makedoc
- xmlwf xmldoc/readme.xml #check for well-formedness
xmllint --noout --valid xmldoc/readme.xml #validate
- xsltproc \
+- xsltproc --load-trace \
++ XML_CATALOG_FILES= xsltproc --load-trace \
--stringparam base.dir "$(WEB)/htmldoc-$(DOCVERSION)/" \
-@@ -246,7 +245,7 @@ changes.html: FORCE
+ --stringparam root.filename "index" \
+ xmldoc/babelmain.xsl \
+@@ -293,7 +292,7 @@ changes.html: FORCE
wget -O $(WEB)/changes.html http://www.gpsbabel.org/changes.html || exit 1
rm -f $(WEB)/changes.html.1 > /dev/null

diff -uNpr gpsbabel/patches/patch-configure_in gpsbabel.new/patches/patch-configure_in
--- gpsbabel/patches/patch-configure_in Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/patches/patch-configure_in Thu Jan 1 09:00:00 1970
@@ -1,64 +0,0 @@
---- configure.in.orig Tue Sep 4 07:09:52 2012
-+++ configure.in Tue Dec 25 21:50:38 2012
-@@ -62,15 +62,20 @@ if test "$cet" = "default"; then
- fi
-
- AC_MSG_CHECKING(whether to support shapefiles)
--AC_ARG_ENABLE(shapefile,
-- [ --enable-shapefile=[(yes)|no]],
-- [ enable_shapefile="$enableval"],[enable_shapefile="yes"])
-- if test "$enable_shapefile" != "no" ; then
-+AC_ARG_WITH(shapefile, [ --enable-shapefile=[(included)|system|no]])
-+ case $with_shapefile in
-+ "system")
-+ AC_CHECK_LIB([shp], [SHPOpen])
- AC_DEFINE(SHAPELIB_ENABLED, 1, [1 to enable shapefile support])
-- AC_MSG_RESULT(yes)
-- else
-+ ;;
-+ "no")
- AC_MSG_RESULT(no)
-- fi
-+ ;;
-+ *) SHAPE="\$(SHAPE)"
-+ AC_DEFINE(SHAPELIB_ENABLED, 1, [1 to enable shapefile support])
-+ AC_MSG_RESULT(using included version)
-+ ;;
-+ esac
-
- AC_MSG_CHECKING(whether to support Palm/OS pdb formats)
- AC_ARG_ENABLE(pdb,
-@@ -223,32 +228,8 @@ AC_SUBST(USB_LIBS)
- AC_SUBST(USB_CFLAGS)
- AC_SUBST(OSJEEPS)
- AC_SUBST(GBSER)
-+AC_SUBST(SHAPE)
- AC_SUBST(ZLIB)
--
--dnl Linux HID support
--case "$target" in
-- *-linux-*)
-- AC_MSG_CHECKING(for Linux HID interface)
-- AC_COMPILE_IFELSE([
-- #include <sys/ioctl.h>
-- #include <linux/types.h>
-- #include <linux/hiddev.h>
-- #include <linux/hidraw.h>
-- void f(void) {
-- struct hidraw_devinfo info;
-- struct hiddev_field_info finfo;
-- struct hiddev_usage_ref_multi urefm;
-- struct hiddev_report_info rinfo;
-- ioctl(0, HIDIOCGRAWINFO, &info);
-- ioctl(0, HIDIOCGFIELDINFO, &finfo);
-- ioctl(0, HIDIOCSUSAGES, &urefm);
-- ioctl(0, HIDIOCSREPORT, &rinfo);
-- }],
-- AC_MSG_RESULT(yes)
-- AC_DEFINE(HAVE_LINUX_HID, 1, [Defined if you have Linux HID]),
-- AC_MSG_RESULT(no))
-- ;;
--esac
-
- AC_MSG_CHECKING(for random stuff to make you feel better)
- AC_MSG_RESULT(failed)
diff -uNpr gpsbabel/patches/patch-gbser_posix_c gpsbabel.new/patches/patch-gbser_posix_c
--- gpsbabel/patches/patch-gbser_posix_c Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/patches/patch-gbser_posix_c Thu Jan 1 09:00:00 1970
@@ -1,11 +0,0 @@
---- gbser_posix.c.orig Tue Jul 26 10:56:33 2011
-+++ gbser_posix.c Tue Dec 25 21:52:11 2012
-@@ -142,7 +142,7 @@ void* gbser_init(const char* port_name)
- if (0 == strcmp(port_name, "-")) {
- h->fd = 0;
- return h;
-- } else if (h->fd = open(port_name, O_RDWR | O_NOCTTY), h->fd == -1) {
-+ } else if (h->fd = open(port_name, O_RDWR | O_NOCTTY | O_NDELAY), h->fd == -1) {
- warning("Failed to open port (%s)\n", strerror(errno));
- goto failed;
- }
diff -uNpr gpsbabel/patches/patch-gbser_posix_cc gpsbabel.new/patches/patch-gbser_posix_cc
--- gpsbabel/patches/patch-gbser_posix_cc Thu Jan 1 09:00:00 1970
+++ gpsbabel.new/patches/patch-gbser_posix_cc Sun Sep 1 07:17:55 2019
@@ -0,0 +1,11 @@
+--- gbser_posix.cc.orig Thu May 2 17:26:47 2019
++++ gbser_posix.cc Sat Aug 24 19:55:42 2019
+@@ -142,7 +142,7 @@ void* gbser_init(const char* port_name)
+ if (0 == strcmp(port_name, "-")) {
+ h->fd = 0;
+ return h;
+- } else if (h->fd = open(port_name, O_RDWR | O_NOCTTY), h->fd == -1) {
++ } else if (h->fd = open(port_name, O_RDWR | O_NOCTTY | O_NDELAY), h->fd == -1) {
+ warning("Failed to open port (%s)\n", strerror(errno));
+ goto failed;
+ }
diff -uNpr gpsbabel/patches/patch-gui_serial_unix_cc gpsbabel.new/patches/patch-gui_serial_unix_cc
--- gpsbabel/patches/patch-gui_serial_unix_cc Thu Jan 1 09:00:00 1970
+++ gpsbabel.new/patches/patch-gui_serial_unix_cc Sun Sep 1 07:17:55 2019
@@ -0,0 +1,21 @@
+--- gui/serial_unix.cc.orig Thu May 2 17:26:47 2019
++++ gui/serial_unix.cc Sat Aug 24 19:55:42 2019
+@@ -84,12 +84,12 @@ static QStringList dynamicDevices()
+
+
+ static const char* deviceNames[] = {
+- "/dev/ttyS0",
+- "/dev/ttyS1",
+- "/dev/ttyS2",
+- "/dev/ttyS3",
+- "/dev/ttyUSB0",
+- "/dev/rfcomm0",
++ "/dev/cua00",
++ "/dev/cua01",
++ "/dev/cua02",
++ "/dev/cua03",
++ "/dev/cuaU0",
++ "/dev/cuaU1",
+ nullptr
+ };
+
diff -uNpr gpsbabel/patches/patch-gui_serial_unix_cpp gpsbabel.new/patches/patch-gui_serial_unix_cpp
--- gpsbabel/patches/patch-gui_serial_unix_cpp Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/patches/patch-gui_serial_unix_cpp Thu Jan 1 09:00:00 1970
@@ -1,22 +0,0 @@
-$OpenBSD: patch-gui_serial_unix_cpp,v 1.1 2012/02/18 22:04:07 sthen Exp $
---- gui/serial_unix.cpp.orig Sun Jan 15 20:10:04 2012
-+++ gui/serial_unix.cpp Sun Jan 15 20:11:26 2012
-@@ -22,12 +22,12 @@
- #if !defined (Q_OS_MAC) // FIXME: find a better way to hide this on Mac.
-
- static const char *deviceNames[] = {
-- "/dev/ttyS0",
-- "/dev/ttyS1",
-- "/dev/ttyS2",
-- "/dev/ttyS3",
-- "/dev/ttyUSB0",
-- "/dev/rfcomm0",
-+ "/dev/cua00",
-+ "/dev/cua01",
-+ "/dev/cua02",
-+ "/dev/cua03",
-+ "/dev/cuaU0",
-+ "/dev/cuaU1",
- 0
- };
-
diff -uNpr gpsbabel/pkg/DESCR-main gpsbabel.new/pkg/DESCR-main
--- gpsbabel/pkg/DESCR-main Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/pkg/DESCR-main Sun Sep 1 07:17:55 2019
@@ -4,4 +4,4 @@ or even a serial upload or download to a GPS unit such
Magellan. By flattening the Tower of Babel that the authors of various programs
for manipulating GPS data have imposed upon us, it returns to us the ability to
freely move our own waypoint data between the programs and hardware we choose to
-use.
\ No newline at end of file
+use.
diff -uNpr gpsbabel/pkg/PLIST-main gpsbabel.new/pkg/PLIST-main
--- gpsbabel/pkg/PLIST-main Sun Sep 1 07:17:49 2019
+++ gpsbabel.new/pkg/PLIST-main Sun Sep 1 07:17:55 2019
@@ -3,232 +3,8 @@
@bin bin/gpsbabel
@comment share/applications/
share/doc/gpsbabel/
-share/doc/gpsbabel/Advanced_Usage.html
-share/doc/gpsbabel/Data_Filters.html
-share/doc/gpsbabel/Datums.html
-share/doc/gpsbabel/Download.html
-share/doc/gpsbabel/GarminIcons.html
-share/doc/gpsbabel/Getting_and_Building.html
-share/doc/gpsbabel/Glossary.html
-share/doc/gpsbabel/Introduction.html
-share/doc/gpsbabel/Invocation.html
share/doc/gpsbabel/README.contrib
share/doc/gpsbabel/README.igc
-share/doc/gpsbabel/README.magnav
share/doc/gpsbabel/README.mapconverter
-share/doc/gpsbabel/README.psp
+share/doc/gpsbabel/README.md
share/doc/gpsbabel/README.xmapwpt
-share/doc/gpsbabel/Route_And_Track_Modes.html
-share/doc/gpsbabel/Source.html
-share/doc/gpsbabel/Styles.html
-share/doc/gpsbabel/Suboptions.html
-share/doc/gpsbabel/The_Formats.html
-share/doc/gpsbabel/The_Problem.html
-share/doc/gpsbabel/The_Solution.html
-share/doc/gpsbabel/Usage.html
-share/doc/gpsbabel/all_options.html
-share/doc/gpsbabel/batchfile.html
-share/doc/gpsbabel/filter_arc.html
-share/doc/gpsbabel/filter_bend.html
-share/doc/gpsbabel/filter_discard.html
-share/doc/gpsbabel/filter_duplicate.html
-share/doc/gpsbabel/filter_height.html
-share/doc/gpsbabel/filter_interpolate.html
-share/doc/gpsbabel/filter_nuketypes.html
-share/doc/gpsbabel/filter_polygon.html
-share/doc/gpsbabel/filter_position.html
-share/doc/gpsbabel/filter_radius.html
-share/doc/gpsbabel/filter_reverse.html
-share/doc/gpsbabel/filter_simplify.html
-share/doc/gpsbabel/filter_sort.html
-share/doc/gpsbabel/filter_stack.html
-share/doc/gpsbabel/filter_swap.html
-share/doc/gpsbabel/filter_track.html
-share/doc/gpsbabel/filter_transform.html
-share/doc/gpsbabel/fmt_alantrl.html
-share/doc/gpsbabel/fmt_alanwpr.html
-share/doc/gpsbabel/fmt_an1.html
-share/doc/gpsbabel/fmt_arc.html
-share/doc/gpsbabel/fmt_axim_gpb.html
-share/doc/gpsbabel/fmt_baroiq.html
-share/doc/gpsbabel/fmt_bcr.html
-share/doc/gpsbabel/fmt_bushnell.html
-share/doc/gpsbabel/fmt_bushnell_trl.html
-share/doc/gpsbabel/fmt_cambridge.html
-share/doc/gpsbabel/fmt_cetus.html
-share/doc/gpsbabel/fmt_coastexp.html
-share/doc/gpsbabel/fmt_compegps.html
-share/doc/gpsbabel/fmt_copilot.html
-share/doc/gpsbabel/fmt_coto.html
-share/doc/gpsbabel/fmt_cst.html
-share/doc/gpsbabel/fmt_csv.html
-share/doc/gpsbabel/fmt_cup.html
-share/doc/gpsbabel/fmt_custom.html
-share/doc/gpsbabel/fmt_delbin.html
-share/doc/gpsbabel/fmt_destinator_itn.html
-share/doc/gpsbabel/fmt_destinator_poi.html
-share/doc/gpsbabel/fmt_destinator_trl.html
-share/doc/gpsbabel/fmt_dg-100.html
-share/doc/gpsbabel/fmt_dg-200.html
-share/doc/gpsbabel/fmt_dmtlog.html
-share/doc/gpsbabel/fmt_dna.html
-share/doc/gpsbabel/fmt_easygps.html
-share/doc/gpsbabel/fmt_enigma.html
-share/doc/gpsbabel/fmt_exif.html
-share/doc/gpsbabel/fmt_flysight.html
-share/doc/gpsbabel/fmt_fugawi.html
-share/doc/gpsbabel/fmt_g7towin.html
-share/doc/gpsbabel/fmt_garmin.html
-share/doc/gpsbabel/fmt_garmin301.html
-share/doc/gpsbabel/fmt_garmin_fit.html
-share/doc/gpsbabel/fmt_garmin_gpi.html
-share/doc/gpsbabel/fmt_garmin_poi.html
-share/doc/gpsbabel/fmt_garmin_txt.html
-share/doc/gpsbabel/fmt_garmin_xt.html
-share/doc/gpsbabel/fmt_gcdb.html
-share/doc/gpsbabel/fmt_gdb.html
-share/doc/gpsbabel/fmt_geo.html
-share/doc/gpsbabel/fmt_geonet.html
-share/doc/gpsbabel/fmt_geoniche.html
-share/doc/gpsbabel/fmt_ggv_log.html
-share/doc/gpsbabel/fmt_ggv_ovl.html
-share/doc/gpsbabel/fmt_glogbook.html
-share/doc/gpsbabel/fmt_gnav_trl.html
-share/doc/gpsbabel/fmt_google.html
-share/doc/gpsbabel/fmt_gopal.html
-share/doc/gpsbabel/fmt_gpilots.html
-share/doc/gpsbabel/fmt_gpl.html
-share/doc/gpsbabel/fmt_gpsdrive.html
-share/doc/gpsbabel/fmt_gpsdrivetrack.html
-share/doc/gpsbabel/fmt_gpsman.html
-share/doc/gpsbabel/fmt_gpspilot.html
-share/doc/gpsbabel/fmt_gpssim.html
-share/doc/gpsbabel/fmt_gpsutil.html
-share/doc/gpsbabel/fmt_gpx.html
-share/doc/gpsbabel/fmt_gtm.html
-share/doc/gpsbabel/fmt_gtrnctr.html
-share/doc/gpsbabel/fmt_gtrnctr1.html
-share/doc/gpsbabel/fmt_hiketech.html
-share/doc/gpsbabel/fmt_holux.html
-share/doc/gpsbabel/fmt_hsandv.html
-share/doc/gpsbabel/fmt_html.html
-share/doc/gpsbabel/fmt_humminbird.html
-share/doc/gpsbabel/fmt_humminbird_ht.html
-share/doc/gpsbabel/fmt_iblue747.html
-share/doc/gpsbabel/fmt_iblue757.html
-share/doc/gpsbabel/fmt_igc.html
-share/doc/gpsbabel/fmt_ignrando.html
-share/doc/gpsbabel/fmt_igo2008_poi.html
-share/doc/gpsbabel/fmt_igo8.html
-share/doc/gpsbabel/fmt_ik3d.html
-share/doc/gpsbabel/fmt_itracku-bin.html
-share/doc/gpsbabel/fmt_itracku.html
-share/doc/gpsbabel/fmt_jogmap.html
-share/doc/gpsbabel/fmt_jtr.html
-share/doc/gpsbabel/fmt_kml.html
-share/doc/gpsbabel/fmt_kompass_tk.html
-share/doc/gpsbabel/fmt_kompass_wp.html
-share/doc/gpsbabel/fmt_ktf2.html
-share/doc/gpsbabel/fmt_kwf2.html
-share/doc/gpsbabel/fmt_land_air_sea.html
-share/doc/gpsbabel/fmt_lmx.html
-share/doc/gpsbabel/fmt_lowranceusr.html
-share/doc/gpsbabel/fmt_lowranceusr4.html
-share/doc/gpsbabel/fmt_m241-bin.html
-share/doc/gpsbabel/fmt_m241.html
-share/doc/gpsbabel/fmt_mag_pdb.html
-share/doc/gpsbabel/fmt_magellan.html
-share/doc/gpsbabel/fmt_magellan1.html
-share/doc/gpsbabel/fmt_magellanx.html
-share/doc/gpsbabel/fmt_maggeo.html
-share/doc/gpsbabel/fmt_magnav.html
-share/doc/gpsbabel/fmt_mapasia_tr7.html
-share/doc/gpsbabel/fmt_mapconverter.html
-share/doc/gpsbabel/fmt_mapsend.html
-share/doc/gpsbabel/fmt_mapsource.html
-share/doc/gpsbabel/fmt_miniHomer.html
-share/doc/gpsbabel/fmt_mmo.html
-share/doc/gpsbabel/fmt_motoactv.html
-share/doc/gpsbabel/fmt_msroute.html
-share/doc/gpsbabel/fmt_msroute1.html
-share/doc/gpsbabel/fmt_mtk-bin.html
-share/doc/gpsbabel/fmt_mtk.html
-share/doc/gpsbabel/fmt_mxf.html
-share/doc/gpsbabel/fmt_navicache.html
-share/doc/gpsbabel/fmt_navigonwpt.html
-share/doc/gpsbabel/fmt_naviguide.html
-share/doc/gpsbabel/fmt_navilink.html
-share/doc/gpsbabel/fmt_navitel_trk.html
-share/doc/gpsbabel/fmt_netstumbler.html
-share/doc/gpsbabel/fmt_nima.html
-share/doc/gpsbabel/fmt_nmea.html
-share/doc/gpsbabel/fmt_nmn4.html
-share/doc/gpsbabel/fmt_openoffice.html
-share/doc/gpsbabel/fmt_osm.html
-share/doc/gpsbabel/fmt_ozi.html
-share/doc/gpsbabel/fmt_palmdoc.html
-share/doc/gpsbabel/fmt_pathaway.html
-share/doc/gpsbabel/fmt_pcx.html
-share/doc/gpsbabel/fmt_pocketfms_bc.html
-share/doc/gpsbabel/fmt_pocketfms_fp.html
-share/doc/gpsbabel/fmt_pocketfms_wp.html
-share/doc/gpsbabel/fmt_psitrex.html
-share/doc/gpsbabel/fmt_psp.html
-share/doc/gpsbabel/fmt_quovadis.html
-share/doc/gpsbabel/fmt_raymarine.html
-share/doc/gpsbabel/fmt_ricoh.html
-share/doc/gpsbabel/fmt_s_and_t.html
-share/doc/gpsbabel/fmt_saplus.html
-share/doc/gpsbabel/fmt_saroute.html
-share/doc/gpsbabel/fmt_sbn.html
-share/doc/gpsbabel/fmt_sbp.html
-share/doc/gpsbabel/fmt_skyforce.html
-share/doc/gpsbabel/fmt_skytraq-bin.html
-share/doc/gpsbabel/fmt_skytraq.html
-share/doc/gpsbabel/fmt_sportsim.html
-share/doc/gpsbabel/fmt_stmsdf.html
-share/doc/gpsbabel/fmt_stmwpp.html
-share/doc/gpsbabel/fmt_subrip.html
-share/doc/gpsbabel/fmt_tabsep.html
-share/doc/gpsbabel/fmt_tef.html
-share/doc/gpsbabel/fmt_teletype.html
-share/doc/gpsbabel/fmt_text.html
-share/doc/gpsbabel/fmt_tiger.html
-share/doc/gpsbabel/fmt_tmpro.html
-share/doc/gpsbabel/fmt_tomtom.html
-share/doc/gpsbabel/fmt_tomtom_asc.html
-share/doc/gpsbabel/fmt_tomtom_itn.html
-share/doc/gpsbabel/fmt_tomtom_itn_places.html
-share/doc/gpsbabel/fmt_tpg.html
-share/doc/gpsbabel/fmt_tpo2.html
-share/doc/gpsbabel/fmt_tpo3.html
-share/doc/gpsbabel/fmt_unicsv.html
-share/doc/gpsbabel/fmt_v900.html
-share/doc/gpsbabel/fmt_vcard.html
-share/doc/gpsbabel/fmt_vidaone.html
-share/doc/gpsbabel/fmt_vitosmt.html
-share/doc/gpsbabel/fmt_vitovtt.html
-share/doc/gpsbabel/fmt_vpl.html
-share/doc/gpsbabel/fmt_wbt-bin.html
-share/doc/gpsbabel/fmt_wbt-tk1.html
-share/doc/gpsbabel/fmt_wbt.html
-share/doc/gpsbabel/fmt_wfff.html
-share/doc/gpsbabel/fmt_wintec_tes.html
-share/doc/gpsbabel/fmt_xcsv.html
-share/doc/gpsbabel/fmt_xmap.html
-share/doc/gpsbabel/fmt_xmap2006.html
-share/doc/gpsbabel/fmt_xmapwpt.html
-share/doc/gpsbabel/fmt_xol.html
-share/doc/gpsbabel/fmt_yahoo.html
-share/doc/gpsbabel/index.html
-share/doc/gpsbabel/inifile.html
-share/doc/gpsbabel/style_behavior.html
-share/doc/gpsbabel/style_define.html
-share/doc/gpsbabel/style_examples.html
-share/doc/gpsbabel/style_global.html
-share/doc/gpsbabel/style_intro2.html
-share/doc/gpsbabel/style_layout.html
-share/doc/gpsbabel/style_notes.html
-share/doc/gpsbabel/styles_internal_const.html
-share/doc/gpsbabel/styles_intro.html
-share/doc/gpsbabel/tracking.html

Regards,

--
SASANO Takayoshi (JG1UAA) <uaa@cvs.openbsd.org>

misc/screen adjustments

We're quite behind on updates for misc/screen, largely because there's
a "screen,shm" FLAVOR including a patch set that is used with misc/brltty
which can't easily be updated.

I'd like to split the patched version into a separate port so that the main
screen port can be updated independently. tgz for the screen-shm port is
attached, and there's a diff inline to remove/adjust the other parts.
(I'll also rm patches/shmpatch-*, but that's uninteresting noise so I've
left it out of the diff).

Any comments/OKs?

Index: misc/Makefile
===================================================================
RCS file: /cvs/ports/misc/Makefile,v
retrieving revision 1.190
diff -u -p -r1.190 Makefile
--- misc/Makefile 14 Aug 2019 18:43:48 -0000 1.190
+++ misc/Makefile 31 Aug 2019 16:38:19 -0000
@@ -94,7 +94,7 @@
SUBDIR += rocrail
SUBDIR += rpm
SUBDIR += screen
- SUBDIR += screen,shm
+ SUBDIR += screen-shm,shm
SUBDIR += sent
SUBDIR += shared-desktop-ontologies
SUBDIR += shared-mime-info
Index: misc/brltty/Makefile
===================================================================
RCS file: /cvs/ports/misc/brltty/Makefile,v
retrieving revision 1.18
diff -u -p -r1.18 Makefile
--- misc/brltty/Makefile 17 Jul 2019 14:46:33 -0000 1.18
+++ misc/brltty/Makefile 31 Aug 2019 16:38:19 -0000
@@ -3,16 +3,17 @@
COMMENT= access software for a blind person using a braille terminal

DISTNAME= brltty-3.6
-REVISION= 3
+REVISION= 4
CATEGORIES= misc
HOMEPAGE= http://mielke.cc/brltty
MASTER_SITES= ${HOMEPAGE}/releases/
+
# GPL
PERMIT_PACKAGE= Yes

WANTLIB= c curses pthread sndio

-RUN_DEPENDS= screen-*-shm:misc/screen,shm
+RUN_DEPENDS= screen-*-shm:misc/screen-shm
USE_GMAKE= Yes
CONFIGURE_STYLE=gnu
CONFIGURE_ARGS= --with-install-root=${WRKINST} \
Index: misc/screen/Makefile
===================================================================
RCS file: /cvs/ports/misc/screen/Makefile,v
retrieving revision 1.70
diff -u -p -r1.70 Makefile
--- misc/screen/Makefile 15 Aug 2019 21:01:49 -0000 1.70
+++ misc/screen/Makefile 31 Aug 2019 16:38:19 -0000
@@ -1,11 +1,10 @@
# $OpenBSD: Makefile,v 1.70 2019/08/15 21:01:49 naddy Exp $
-# Please adjust www/faq/faq15.html if updating.

COMMENT= multi-screen window manager

VERSION= 4.0.3
DISTNAME= screen-${VERSION}
-REVISION= 7
+REVISION= 8
CATEGORIES= misc
MASTER_SITES= ${MASTER_SITE_GNU:=screen/}

@@ -21,16 +20,13 @@ CONFIGURE_STYLE= autoconf no-autoheader
CONFIGURE_ARGS= --with-sys-screenrc="${SYSCONFDIR}/screenrc"
USE_GROFF = Yes

-FLAVORS= static shm
+FLAVORS= static
FLAVOR?=

.if ${FLAVOR} == "static"
CONFIGURE_ENV= LDFLAGS="${STATIC}"
.else
WANTLIB= c curses util
-.endif
-.if ${FLAVOR} == "shm"
-PATCH_LIST= patch-* shmpatch-*
.endif

ALL_TARGET= screen screen.info
Index: misc/screen/pkg/DESCR
===================================================================
RCS file: /cvs/ports/misc/screen/pkg/DESCR,v
retrieving revision 1.5
diff -u -p -r1.5 DESCR
--- misc/screen/pkg/DESCR 22 Nov 2003 00:56:58 -0000 1.5
+++ misc/screen/pkg/DESCR 31 Aug 2019 16:38:20 -0000
@@ -9,4 +9,3 @@ regions between windows.

Flavors:
static - Build with statically linked binaries.
- shm - export screen as shared memory, useful for brltty.

Re: update math/coq

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

> On Fri, Aug 30, 2019 at 10:01:59AM +0200, Christopher Zimmermann wrote:
........
> > I'd like to update math/coq to 8.10+beta2. Which is needed to support
> > OCaml 4.08. The only user of coq is lang/compcert and was already
> > updated to support Coq 8.10 and OCaml 4.08.
> > When this update and the devel/frama-c update are committed the OCaml
> > 4.08 update can go in. Tested on amd64 with and without nativecode. OKs?

OK!

-- yozo.

-----BEGIN PGP SIGNATURE-----

iQJJBAEBCgAzFiEEsSBE3BD3oI0EPJSvM6KY3A5GNSgFAl1qjogVHHlvem9AdjAw
Ny52YWlvLm5lLmpwAAoJEDOimNwORjUoA/0P/AhMya6BEAXObFqgozsFMdwXAJiI
tWtSMTkvPcTOQRqOT4bfxmNf2t9cM0qIvykF7Pt0yuiHBD+fOhQzq+Rf39R6pCrT
+tT5p7jCY1s//yL31YadJZsGUGwKcHV1gvWnYzR6wAGa723jRCrjD+iGgvOidQQ8
+4iJp+vTI901h5vfSI9UU1YdjDhATBx31xpNUraNctJhzRDsjwCWgQtPw+nTrAaS
oaiJIHDyml5FpiL+Iw6FJ4daPsLNTz609T8W5aCRwxhd+Nf0VeXWJMDt8ouoEJUP
/iSDMIsyxHwjcTMwYp9wymXlb/tVyTZnsHf5BSXv3OId3rop2sxPdp3RhMlRPHvJ
gqLNdZECHGOCdMxKHUCTr4sKD7yST3LW2DP39Crx9NCIrs9WIkDXPQfrMD04Kr0n
HDhAvscisPnwRKEap13zs3lPjbpLUCZcHvBEuNOIg2CQ90jglroqvHaEEaXuA9WV
3+JdE+Oy929p1N/BE9jRNmIiViAVnc+f+ZZgE2eH0lI0dX1IEAIuTl/8CPBV3Xfb
fXS29+ZPmJ/MMsIHb4nwtc3TpIOR+iiSRdaATNMfVnQi/2OMRnvY6Nb9cPJX5SvC
YncYs1+O5gyCgCgUcl3+DHpntsOAO7k81jKd0zmUKw8iTUFPz8azoyAOJy4eGY0h
JBiE37xRK1Pva5n/
=bKPP
-----END PGP SIGNATURE-----

Re: Incoming connection via VLAN

On 2019-08-30, Felix Hanley <felix@userspace.com.au> wrote:
> Hello all,
>
> My home internet connection (Internode Australia) has recently been
> "upgraded" and is now delivered via vlan ID 2. Previously had the
> following configuration which worked without issue:
>
> # cat /etc/hostname.em0
> up
>
> # cat /etc/hostname.pppoe0
> inet 0.0.0.0 255.255.255.255 NONE \
> pppoedev em0 authproto pap \
> authname 'XXXX@internode.on.net' \
> authkey 'XXXX' up
> dest 0.0.0.1
> inet6 eui64
> !/sbin/route add default -ifp pppoe0 0.0.0.1
> !/sbin/route add -inet6 default -ifp pppoe0 fe80::%pppoe0
> !/etc/rc.d/dhcp6c restart
> !/sbin/pfctl -ef /etc/pf.conf
>
> After working out the vlan stuff I now have the following:
>
> # cat /etc/hostname.em0
> up
>
> # cat /etc/hostname.vlan2
> vnetid 2 parent em0 txprio 1
> up
>
> # cat /etc/hostname.pppoe0
> inet 0.0.0.0 255.255.255.255 NONE \
> llprio 1 mtu 1440 \
> pppoedev vlan2 authproto pap \
> authname 'XXXX@internode.on.net' \
> authkey 'XXXX' up
> dest 0.0.0.1
> inet6 eui64
> !/sbin/route add default -ifp pppoe0 0.0.0.1
> !/sbin/route add -inet6 default -ifp pppoe0 fe80::%pppoe0
> !/etc/rc.d/dhcp6c restart
> !/sbin/pfctl -ef /etc/pf.conf
>
> I am able to access the internet fine. My problem is incoming
> connections are unable to access the OBSD router but are able to be
> redirected to internal hosts just fine. There was no problems with this
> prior to the vlan stuff. My stripped down pf.conf is:
>
> # cat /etc/pf.conf
> egress = "pppoe0"
> zappa = "10.0.1.2"
>
> set skip on lo
> set skip on vlan2
> set block-policy drop
> set loginterface $egress
>
> queue outq on $egress bandwidth 13M max 13M flows 1024 qlimit 1024 default
>
> match in inet all scrub (no-df random-id)
> match on $egress inet scrub (max-mss 1440)
> # NAT all outbound IPv4 traffic from the rest of our network
> match out on $egress inet from !($egress:network) to any nat-to ($egress:0)
>
> antispoof quick for lo
>

I'd suggest adding "block all" or "block log all" here. That way you can be
sure that any traffic making it through the ruleset has been permitted by one
of the following "pass" rules (which are stateful rules). Otherwise things
might only be making it through due to the implicit default-permit rule
which is not stateful.

> pass in on $egress proto { tcp udp } from any to ($egress) port { ssh
> http https }
> pass in on $egress proto tcp from any to ($egress) port 51022 rdr-to
> $zappa port ssh
>
> Running tcpdump on pppoe0 show ICMP packets but never any SSH (or other
> TCP) packets coming in on egress. I am confused that rdr-to works but
> not connections to the router do not.
>
> Any help would be greatly appreciated.
>
> -felix
>
>

It's odd that you don't see any TCP packets coming in on pppoe0 with
tcpdump; does that even include port 51022 if you're connected via
the rdr-to?

Re: update: textproc/ripgrep

On Sat, 31 Aug 2019, Sebastien Marie wrote:

> I just commited your diff, with few changes to keep libc updated to
> 0.2.63 in order to keep sparc64 support.

Thank you Sebastien.

--
Paco Esteban.
https://onna.be/gpgkey.asc
9A6B 6083 AD9E FDC2 0EAF 5CB3 5818 130B 8A6D BC03

Re: Support new

On Sat, Aug 31, 2019 at 09:58:29AM +0800, Muhammad Muntaza wrote:
> 0
> C Indonesia
> P South Kalimantan
> T Banjarbaru
> Z 70724
> O Consultant
> I Muhammad Muntaza bin Hatta
> A Jalan Kawamara, Komplek Citra Pesona Mandiri Asri, Landasan Ulin
> M muhammad@muntaza.id
> U https://www.muntaza.id/openbsd
> B +62 816 20 6441
> X
> N OpenBSD Consulting, Training, Installation, Maintenance and Support for
> mid-size business. Over 10 years of experience with OpenBSD and PF firewall.

Added, thank you.

Friday, August 30, 2019

Re: update: textproc/ripgrep

On Thu, Aug 29, 2019 at 06:10:44PM +0200, Paco Esteban wrote:
> On Sun, 18 Aug 2019, Paco Esteban wrote:
>
> > Hi ports@,
> >
> > Here's an update for textproc/ripgrep from 0.10.0 to 11.0.2. I's only
> > one major version upgrade, but they changed the versioning scheme:
> >
> > https://github.com/BurntSushi/ripgrep/issues/1172
> >
> > You can find here the changelog:
> >
> > https://github.com/BurntSushi/ripgrep/blob/11.0.2/CHANGELOG.md
> >
> > This port does not have consumers. All regression tests pass and it
> > works well for me on amd64.
> >
> > I have to say I did not try it extensively, as I mostly use it as
> > "grepprg" for vim.
>
> ping ?

I just commited your diff, with few changes to keep libc updated to
0.2.63 in order to keep sparc64 support.

Thanks.
--
Sebastien Marie

Re: What is you motivational to use OpenBSD

I first started using it around version 4.3. I was trying BSD's after
using Linux for a bit, and tried FreeBSD first.

But OpenBSD was the only one that supported my laptop's WiFi card. And
getting everything running was much less of a hassle.

It's the best BSD for getting a fine workstation up quickly.

My Thinkpad T60 running OpenBSD got me through college just fine.

It's the first operating system that I was able to do lots of cool
sysadmin stuff because of how simple it is.

And also the first operating system I found that was easier to find
answers in the manual, and not through Google.

Also the OS that inspired me to learn C programming.

OpenBSD is the best BSD, and getting better every release.

Support new

0
C Indonesia
P South Kalimantan
T Banjarbaru
Z 70724
O Consultant
I Muhammad Muntaza bin Hatta
A Jalan Kawamara, Komplek Citra Pesona Mandiri Asri, Landasan Ulin
M muhammad@muntaza.id
U https://www.muntaza.id/openbsd
B +62 816 20 6441
X
N OpenBSD Consulting, Training, Installation, Maintenance and Support for
mid-size business. Over 10 years of experience with OpenBSD and PF firewall.

support new

0
C Indonesia
P South Kalimantan
T Banjarbau
Z 70724
O Consultant
I Muhammad Muntaza bin Hatta
A Jalan Kawamara, Komplek Citra Pesona Mandiri Asri, Landasan Ulin
M muhammad@muntaza.id
U https://www.muntaza.id/openbsd
B +62 816 20 6441
X
N OpenBSD Consulting, Training, Installation, Maintenance and Support for
mid-size business. Over 10 years of experience with OpenBSD and PF firewall.

Re: seafile-daemon-6.2.11 "cannot import name NamedPipeClient"

On 2019/08/30 17:27, niklasanderson@pm.me wrote:
> Jeremie,
>
> Understood. But I think my confusion is in the fact that there is no update for a broken package when I use the latest release. I've read through a lot of OpenBSD's docs but Im not experienced enough to put all the details together.
>
> If I stick with my current install, am I going to have to compile the correct version of libsearpc myself to workaround the issue?

releases are a fixed point in time and get no updates.

-stable continues from releases and gets limited updates, mostly
security, or occasionally other fixes that affect a wide number of
users. Between around the 4.6 release until very recently, for
packaged software (rather than the base OS) binaries weren't available,
you had to build them yourself.

> Am I correct in my understanding that a standard 6.5 install is part of the -stable release? Are only security patches backported then, and not fixes for broken ports?
>
> Or am I unwittingly on -release, and would have to otherwise wait until a release upgrade is available?

-stable is the cvs branch where post-release fixes are committed.
For the base OS binaries are available for the most recent two releases
on selected arches via sysupgrade. For packages binaries are built from
the -stable branch on amd64/arm64/i386; pkg_add will pick them up
automatically. Primarily only security fixes are committed to this branch.

At present for libsearpc you'll either need to use a -current snapshot
or backport yourself from -current to -stable.

> I apologize for the elementary questions, and I appreciate the help. Thank you.-------- Original Message --------
> On Aug 30, 2019, 3:50 AM, Jeremie Courreges-Anglas wrote:
>
> > On Fri, Aug 30 2019, niklasanderson@pm.me wrote:
> >> Hi everyone,
> >>
> >> The issue Im having goes back to an earlier thread relating to the current release of the Seafile daemon version 6.2.11 (see here: https://marc.info/?l=openbsd-ports&m=155841015232720&w=2)
> >>
> >> To summarize, after installing the seafile-daemon, the seaf-cli option
> >> is available to configure and setup a Seafile server (as I understand
> >> it). The seaf-cli python scripts are broken as discussed in this earlier
> >> exchange: the throw a python error "ImportError: cannot import name
> >> NamedPipeClient" after a script fails to name all relevant files.
> >>
> >> I'm getting this exact issue on OpenBSD 6.5, and I am confused as to
> >> whether or not it has been fixed, or if there is something I need to do
> >> to apply the fix. The original port seemed to have resulted in a fix,
> >> but this fix doesn't appear to be present in a very recent install of
> >> this package.
> >
> > You're on 6.5, which doesn't have the fix. As said by kirby@ in
> >
> > https://marc.info/?l=openbsd-ports&m=155854474314128&w=2
> >
> > you'd need at least libsearpc-3.1p1.
> >
> > --
> > jca | PGP : 0x1524E7EE / 5135 92C1 AD[36 5293 2](tel:3652932)BDF DDCC 0DFA 74AE 1524 E7EE

Re: [Update] databases/p5-Mojo-Pg : Update to 4.15

On Fri, Aug 30, 2019 at 2:22 PM Charlene Wendling <julianaito@posteo.jp>
wrote:

> Hi,
>
> On Fri, 30 Aug 2019 13:32:52 -0500
> Abel Abraham Camarillo Ojeda wrote:
>
> > On Friday, August 30, 2019, wen heping <wenheping2000@hotmail.com>
> > wrote:
> >
> > > Hi,
> > >
> > > Here is a patch for databases/p5-Mojo-Pg:
> > > i) Update to 4.15
> > > ii) Fix LICENSE to artistic 2.0
> > >
> >
> > Hi Wen,
> >
> > I think that perl implied artistic 2.0, is that on longer true? (Or
> > has it never been true? )
>
> It's true, but artistic 2.0 per se does not imply Perl as a license
> marker (may it be for CPAN or for us).
>
> Perl is distributed under either the GPL or Artistic 2.0 [0], and only
> modules mentioning the dual licensing, or the famous "under the same
> terms as Perl itself" should have the Perl license marker.
>
> Mojo-Pg is released only under the term of the Artistic 2.0 license
> [1], so the fix is real.
>

You are correct. OK maintaner

thanks

>
> OK cwen@
>
>
> [0] https://dev.perl.org/licenses/
> [1] https://metacpan.org/pod/Mojo::Pg#COPYRIGHT-AND-LICENSE
>
>

Re: [Update] databases/p5-Mojo-Pg : Update to 4.15

Hi,

On Fri, 30 Aug 2019 13:32:52 -0500
Abel Abraham Camarillo Ojeda wrote:

> On Friday, August 30, 2019, wen heping <wenheping2000@hotmail.com>
> wrote:
>
> > Hi,
> >
> > Here is a patch for databases/p5-Mojo-Pg:
> > i) Update to 4.15
> > ii) Fix LICENSE to artistic 2.0
> >
>
> Hi Wen,
>
> I think that perl implied artistic 2.0, is that on longer true? (Or
> has it never been true? )

It's true, but artistic 2.0 per se does not imply Perl as a license
marker (may it be for CPAN or for us).

Perl is distributed under either the GPL or Artistic 2.0 [0], and only
modules mentioning the dual licensing, or the famous "under the same
terms as Perl itself" should have the Perl license marker.

Mojo-Pg is released only under the term of the Artistic 2.0 license
[1], so the fix is real.

OK cwen@

[0] https://dev.perl.org/licenses/
[1] https://metacpan.org/pod/Mojo::Pg#COPYRIGHT-AND-LICENSE

Re: seafile-daemon-6.2.11 "cannot import name NamedPipeClient"

Ignore my previous email. I rushed to get an answer.

I reviewed the documentation and realize that I had been seriously confused as to how-stable and port management works.

-------- Original Message --------
On Aug 30, 2019, 10:27 AM, wrote:

> Jeremie,
>
> Understood. But I think my confusion is in the fact that there is no update for a broken package when I use the latest release. I've read through a lot of OpenBSD's docs but Im not experienced enough to put all the details together.
>
> If I stick with my current install, am I going to have to compile the correct version of libsearpc myself to workaround the issue?
>
> Am I correct in my understanding that a standard 6.5 install is part of the -stable release? Are only security patches backported then, and not fixes for broken ports?
>
> Or am I unwittingly on -release, and would have to otherwise wait until a release upgrade is available?
>
> I apologize for the elementary questions, and I appreciate the help. Thank you.-------- Original Message --------
> On Aug 30, 2019, 3:50 AM, Jeremie Courreges-Anglas wrote:
>
>> On Fri, Aug 30 2019, niklasanderson@pm.me wrote:
>>> Hi everyone,
>>>
>>> The issue Im having goes back to an earlier thread relating to the current release of the Seafile daemon version 6.2.11 (see here: https://marc.info/?l=openbsd-ports&m=155841015232720&w=2)
>>>
>>> To summarize, after installing the seafile-daemon, the seaf-cli option
>>> is available to configure and setup a Seafile server (as I understand
>>> it). The seaf-cli python scripts are broken as discussed in this earlier
>>> exchange: the throw a python error "ImportError: cannot import name
>>> NamedPipeClient" after a script fails to name all relevant files.
>>>
>>> I'm getting this exact issue on OpenBSD 6.5, and I am confused as to
>>> whether or not it has been fixed, or if there is something I need to do
>>> to apply the fix. The original port seemed to have resulted in a fix,
>>> but this fix doesn't appear to be present in a very recent install of
>>> this package.
>>
>> You're on 6.5, which doesn't have the fix. As said by kirby@ in
>>
>> https://marc.info/?l=openbsd-ports&m=155854474314128&w=2
>>
>> you'd need at least libsearpc-3.1p1.
>>
>> --
>> jca | PGP : 0x1524E7EE / 5135 92C1 AD[36 5293 2](tel:3652932)BDF DDCC 0DFA 74AE 1524 E7EE

Re: [Update] databases/p5-Mojo-Pg : Update to 4.15

On Friday, August 30, 2019, wen heping <wenheping2000@hotmail.com> wrote:

> Hi,
>
> Here is a patch for databases/p5-Mojo-Pg:
> i) Update to 4.15
> ii) Fix LICENSE to artistic 2.0
>

Hi Wen,

I think that perl implied artistic 2.0, is that on longer true? (Or has it
never been true? )

Apart from that reads ok to me.

Regards

> iii) Add TEST_POD=yes to MAKE_ENV
>
> It build well and passed all tests on amd64-head system.
> No other ports depends on it.
>
> Comments? OK?
> wen
>

Re: seafile-daemon-6.2.11 "cannot import name NamedPipeClient"

Jeremie,

Understood. But I think my confusion is in the fact that there is no update for a broken package when I use the latest release. I've read through a lot of OpenBSD's docs but Im not experienced enough to put all the details together.

If I stick with my current install, am I going to have to compile the correct version of libsearpc myself to workaround the issue?

Am I correct in my understanding that a standard 6.5 install is part of the -stable release? Are only security patches backported then, and not fixes for broken ports?

Or am I unwittingly on -release, and would have to otherwise wait until a release upgrade is available?

I apologize for the elementary questions, and I appreciate the help. Thank you.-------- Original Message --------
On Aug 30, 2019, 3:50 AM, Jeremie Courreges-Anglas wrote:

> On Fri, Aug 30 2019, niklasanderson@pm.me wrote:
>> Hi everyone,
>>
>> The issue Im having goes back to an earlier thread relating to the current release of the Seafile daemon version 6.2.11 (see here: https://marc.info/?l=openbsd-ports&m=155841015232720&w=2)
>>
>> To summarize, after installing the seafile-daemon, the seaf-cli option
>> is available to configure and setup a Seafile server (as I understand
>> it). The seaf-cli python scripts are broken as discussed in this earlier
>> exchange: the throw a python error "ImportError: cannot import name
>> NamedPipeClient" after a script fails to name all relevant files.
>>
>> I'm getting this exact issue on OpenBSD 6.5, and I am confused as to
>> whether or not it has been fixed, or if there is something I need to do
>> to apply the fix. The original port seemed to have resulted in a fix,
>> but this fix doesn't appear to be present in a very recent install of
>> this package.
>
> You're on 6.5, which doesn't have the fix. As said by kirby@ in
>
> https://marc.info/?l=openbsd-ports&m=155854474314128&w=2
>
> you'd need at least libsearpc-3.1p1.
>
> --
> jca | PGP : 0x1524E7EE / 5135 92C1 AD[36 5293 2](tel:3652932)BDF DDCC 0DFA 74AE 1524 E7EE

Re: PowerDNS Recursor 4.2.0

On Fri, Aug 30, 2019 at 05:34:03PM +0100, Stuart Henderson wrote:

> On 2019/08/30 16:25, Otto Moerbeek wrote:
> > Hi,
> >
> > just released. This is s strightforward port, I left some new features out
> > for the moment.
>
> s/recursor/auth/ :)

heh, glad you're paying attention ;-)

>
> > Al local patches have been upstreamed.
>
> It now picks up libcurl if present (used by sdig). Here's a diff on top of
> yours to fix up the library dependencies (the -mysql and -ldap ones also
> changed slightly due to other changes in the ports tree). OK sthen with that
> applied on top; otherwise if you prefer it looks like the curl support could
> be disabled via autoconf.

I'd rather keep it, since it is used by the DNS over HTTP code, it is
nice to have a client being able talk that.

>
> "make port-lib-depends-check" still complains about the heimdal libraries,
> but that is a limitation of the checker which doesn't correctly handle
> libraries in subdirs and can be ignored.

OK, I'll test your changes here and commit.

Thanks,

-Otto

>
> --- Makefile- Fri Aug 30 17:24:25 2019
> +++ Makefile Fri Aug 30 17:24:08 2019
> @@ -27,10 +27,11 @@ MULTI_PACKAGES= -main -mysql -pgsql -ldap
> # GPLv2 only, OpenSSL exemption
> PERMIT_PACKAGE= Yes
>
> -WANTLIB += m pthread ${COMPILER_LIBCXX}
> +WANTLIB += crypto m pthread ssl ${COMPILER_LIBCXX}
>
> WANTLIB-main += ${WANTLIB}
> -WANTLIB-main += boost_program_options-mt c crypto sodium sqlite3 z
> +WANTLIB-main += boost_program_options-mt c curl nghttp2 sodium
> +WANTLIB-main += sqlite3 z
>
> MASTER_SITES= https://downloads.powerdns.com/releases/
> MAINTAINER= Otto Moerbeek <otto@drijf.net>
> @@ -42,6 +43,7 @@ NO_TEST= Yes
> LIB_DEPENDS-main= ${LIB_DEPENDS} \
> databases/sqlite3 \
> devel/boost \
> + net/curl \
> security/libsodium
>
> PSEUDO_FLAVORS+= no_mysql no_pgsql no_ldap
> @@ -79,7 +81,7 @@ CONFIGURE_ARGS+= --without-mysql
> LIB_DEPENDS-mysql= ${LIB_DEPENDS} \
> databases/mariadb
> RUN_DEPENDS-mysql= net/powerdns
> -WANTLIB-mysql+= ${WANTLIB} crypto lib/mysql/mysqlclient ssl z
> +WANTLIB-mysql+= ${WANTLIB} iconv mariadb z
>
> # PostgreSQL
> .if ${BUILD_PACKAGES:M-pgsql}
> @@ -91,7 +93,7 @@ CONFIGURE_ARGS+= --without-pg-config
> LIB_DEPENDS-pgsql= ${LIB_DEPENDS} \
> databases/postgresql,-main
> RUN_DEPENDS-pgsql= net/powerdns
> -WANTLIB-pgsql= ${WANTLIB} crypto pq>=2 ssl
> +WANTLIB-pgsql= ${WANTLIB} pq>=2
>
> # LDAP
> .if ${BUILD_PACKAGES:M-ldap}
> @@ -104,7 +106,7 @@ LIB_DEPENDS-ldap= ${LIB_DEPENDS} \
> security/heimdal,-libs
> RUN_DEPENDS-ldap= net/powerdns
> WANTLIB-ldap= ${WANTLIB} ldap_r
> -WANTLIB-ldap+= c com_err crypto lber-2.4 ldap_r-2.4 sasl2 ssl util
> +WANTLIB-ldap+= c com_err lber sasl2 util
> WANTLIB-ldap+= heimdal/lib/asn1 heimdal/lib/hcrypto heimdal/lib/heimbase
> WANTLIB-ldap+= heimdal/lib/heimsqlite heimdal/lib/hx509 heimdal/lib/krb5
> WANTLIB-ldap+= heimdal/lib/roken heimdal/lib/wind
>
>

preview, rspamd update

I've been running various versions of this locally for a while, thought I'd
send it out in case anyone else is interested in testing. rspamd has switched
from libevent to their own copy of libev and the neural network parts (if you
use them) have changed to a different backend.

Index: Makefile
===================================================================
RCS file: /cvs/ports/mail/rspamd/Makefile,v
retrieving revision 1.71
diff -u -p -r1.71 Makefile
--- Makefile 3 Jun 2019 16:06:52 -0000 1.71
+++ Makefile 30 Aug 2019 17:01:15 -0000
@@ -4,7 +4,9 @@ COMMENT= event-driven spam filtering sys

GH_ACCOUNT= vstakhov
GH_PROJECT= rspamd
-GH_TAGNAME= 1.9.4
+#GH_TAGNAME= 1.9.4
+GH_COMMIT= d1ad30ae1aad11e4bde0d889d9fd19b1fe41c499
+DISTNAME= rspamd-2.0.0pre20190830

CATEGORIES= mail

@@ -15,8 +17,8 @@ MAINTAINER= Stuart Henderson <sthen@open
# Apache License 2.0
PERMIT_PACKAGE= Yes

-WANTLIB += c crypto event glib-2.0 gthread-2.0 icudata icui18n icuuc
-WANTLIB += intl m magic pcre pthread sqlite3 ssl z
+WANTLIB += blas c crypto glib-2.0 icudata icui18n icuuc intl m magic
+WANTLIB += pcre sodium sqlite3 ssl z

FLAVORS= no_luajit
.if ${MACHINE_ARCH} == "amd64" || ${MACHINE_ARCH} == "i386"
@@ -32,7 +34,14 @@ LIB_DEPENDS= databases/sqlite3 \
devel/glib2 \
devel/libmagic \
devel/pcre \
+ security/libsodium \
textproc/icu4c
+
+# uses cblas headers; pull this in via LDEP and register an "extra" dependency
+# on cblas lib to make sure rspamd gets updated for major changes in cblas
+LIB_DEPENDS+= math/cblas
+WANTLIB+= cblas
+
BUILD_DEPENDS+= devel/ragel
# /var/rspamd needs to exist for tests to run
TEST_DEPENDS= ${FULLPKGNAME}:${FULLPKGPATH}
@@ -48,25 +57,19 @@ CONFIGURE_ARGS+= -DOPENBSD_BUILD=1 \
-DLOGDIR="${LOCALSTATEDIR}/log/rspamd" \
-DMANDIR="${PREFIX}/man" \
-DRUNDIR="${LOCALSTATEDIR}/run/rspamd" \
- -DRSPAMD_USER="_rspamd" \
- -DRSPAMD_GROUP="_rspamd"
+ -DRSPAMD_USER="_rspamd"

.if ${FLAVOR:Mno_luajit}
-CONFIGURE_ARGS+= -DENABLE_LUAJIT=0 \
- -DENABLE_TORCH=0
+CONFIGURE_ARGS+= -DENABLE_LUAJIT=0
MODULES+= lang/lua
MODLUA_VERSION= 5.3
MODLUA_SA= Yes # avoid overwriting FULLPKGNAME
LIB_DEPENDS+= ${MODLUA_LIB_DEPENDS}
WANTLIB+= ${MODLUA_WANTLIB}
.else
-LIB_DEPENDS+= lang/luajit \
- math/lapack
-WANTLIB+= blas lapack luajit-5.1
+LIB_DEPENDS+= lang/luajit
+WANTLIB+= luajit-5.1
.endif
-
-# Make sure we pick up the base libevent, never the ports one!
-CONFIGURE_ARGS+= -DLIBEVENT_ROOT_DIR=/usr

# Make sure you have no rspamd or redis instances running and note that the
# test suite uses the network.
Index: distinfo
===================================================================
RCS file: /cvs/ports/mail/rspamd/distinfo,v
retrieving revision 1.48
diff -u -p -r1.48 distinfo
--- distinfo 26 May 2019 12:49:36 -0000 1.48
+++ distinfo 30 Aug 2019 17:01:15 -0000
@@ -1,2 +1,2 @@
-SHA256 (rspamd-1.9.4.tar.gz) = 5HIMH0Xe/QfdF7lWPQ3cSAxwvq28GoMyNcB3lgCS4DA=
-SIZE (rspamd-1.9.4.tar.gz) = 4476230
+SHA256 (rspamd-2.0.0pre20190830-d1ad30ae.tar.gz) = WHZzlLFmNCSV1eFDWo/+sHtcet///bc/jIOtY/cdEmo=
+SIZE (rspamd-2.0.0pre20190830-d1ad30ae.tar.gz) = 4031092
Index: patches/patch-CMakeLists_txt
===================================================================
RCS file: /cvs/ports/mail/rspamd/patches/patch-CMakeLists_txt,v
retrieving revision 1.22
diff -u -p -r1.22 patch-CMakeLists_txt
--- patches/patch-CMakeLists_txt 18 Apr 2019 16:12:15 -0000 1.22
+++ patches/patch-CMakeLists_txt 30 Aug 2019 17:01:15 -0000
@@ -6,7 +6,7 @@ both libevent from base *and* libevent2
Index: CMakeLists.txt
--- CMakeLists.txt.orig
+++ CMakeLists.txt
-@@ -517,14 +517,14 @@ SET(POE_LOOP "Loop::IO_Poll")
+@@ -497,10 +497,10 @@ SET(POE_LOOP "Loop::IO_Poll")
SET(TAR "tar")

# Platform specific configuration
@@ -14,50 +14,23 @@ Index: CMakeLists.txt
+IF(CMAKE_SYSTEM_NAME MATCHES "FreeBSD|DragonFly")
ADD_DEFINITIONS(-DFREEBSD -D_BSD_SOURCE)
CONFIGURE_FILE(freebsd/rspamd.sh.in freebsd/rspamd @ONLY)
-
- IF(ENABLE_REDIRECTOR MATCHES "ON")
- CONFIGURE_FILE(freebsd/redirector.sh.in freebsd/redirector @ONLY)
- ENDIF(ENABLE_REDIRECTOR MATCHES "ON")
- MESSAGE(STATUS "Configuring for BSD system")
+ MESSAGE(STATUS "Configuring for FreeBSD/DragonFly system")
# Find util library
ProcessPackage(LIBUTIL LIBRARY util INCLUDE libutil.h
ROOT ${LIBUTIL_ROOT_DIR} OPTIONAL)
-@@ -540,8 +540,14 @@ IF(CMAKE_SYSTEM_NAME MATCHES "^.*BSD$|DragonFly")
+@@ -515,7 +515,13 @@ IF(CMAKE_SYSTEM_NAME MATCHES "^.*BSD$|DragonFly")
ENDIF()
SET(POE_LOOP "Loop::Kqueue")
SET(TAR "gtar")
-ENDIF()
+ENDIF(CMAKE_SYSTEM_NAME MATCHES "FreeBSD|DragonFly")
-
++
+IF(CMAKE_SYSTEM_NAME MATCHES "NetBSD|OpenBSD")
+ MESSAGE(STATUS "Configuring for NetBSD/OpenBSD")
+ SET(POE_LOOP "Loop::Kqueue")
+ SET(TAR "gtar")
+ENDIF(CMAKE_SYSTEM_NAME MATCHES "NetBSD|OpenBSD")
-+
- IF(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
- SET(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -D_BSD_SOURCE -DDARWIN")
- SET(CMAKE_SHARED_LIBRARY_CREATE_C_FLAGS "${CMAKE_SHARED_LIBRARY_CREATE_C_FLAGS} -undefined dynamic_lookup")
-@@ -655,7 +661,7 @@ ELSE()
- ENDIF()

- ProcessPackage(LIBEVENT LIBRARY event INCLUDE event.h INCLUDE_SUFFIXES include/event
-- ROOT ${LIBEVENT_ROOT_DIR} MODULES event libevent)
-+ ROOT ${LIBEVENT_ROOT_DIR} MODULES event)
- ProcessPackage(SQLITE3 LIBRARY sqlite3 INCLUDE sqlite3.h INCLUDE_SUFFIXES include/sqlite3 include/sqlite
- ROOT ${SQLITE3_ROOT_DIR} MODULES sqlite3 sqlite)
- ProcessPackage(ICUDATA LIBRARY icudata INCLUDE unicode/ucnv.h
-@@ -1083,9 +1089,9 @@ CHECK_C_SOURCE_COMPILES ("#include <event.h>
- #error Unsupported
-

Re: PowerDNS Recursor 4.2.0

On 2019/08/30 16:25, Otto Moerbeek wrote:
> Hi,
>
> just released. This is s strightforward port, I left some new features out
> for the moment.

s/recursor/auth/ :)

> Al local patches have been upstreamed.

It now picks up libcurl if present (used by sdig). Here's a diff on top of
yours to fix up the library dependencies (the -mysql and -ldap ones also
changed slightly due to other changes in the ports tree). OK sthen with that
applied on top; otherwise if you prefer it looks like the curl support could
be disabled via autoconf.

"make port-lib-depends-check" still complains about the heimdal libraries,
but that is a limitation of the checker which doesn't correctly handle
libraries in subdirs and can be ignored.

--- Makefile- Fri Aug 30 17:24:25 2019
+++ Makefile Fri Aug 30 17:24:08 2019
@@ -27,10 +27,11 @@ MULTI_PACKAGES= -main -mysql -pgsql -ldap
# GPLv2 only, OpenSSL exemption
PERMIT_PACKAGE= Yes

-WANTLIB += m pthread ${COMPILER_LIBCXX}
+WANTLIB += crypto m pthread ssl ${COMPILER_LIBCXX}

WANTLIB-main += ${WANTLIB}
-WANTLIB-main += boost_program_options-mt c crypto sodium sqlite3 z
+WANTLIB-main += boost_program_options-mt c curl nghttp2 sodium
+WANTLIB-main += sqlite3 z

MASTER_SITES= https://downloads.powerdns.com/releases/
MAINTAINER= Otto Moerbeek <otto@drijf.net>
@@ -42,6 +43,7 @@ NO_TEST= Yes
LIB_DEPENDS-main= ${LIB_DEPENDS} \
databases/sqlite3 \
devel/boost \
+ net/curl \
security/libsodium

PSEUDO_FLAVORS+= no_mysql no_pgsql no_ldap
@@ -79,7 +81,7 @@ CONFIGURE_ARGS+= --without-mysql
LIB_DEPENDS-mysql= ${LIB_DEPENDS} \
databases/mariadb
RUN_DEPENDS-mysql= net/powerdns
-WANTLIB-mysql+= ${WANTLIB} crypto lib/mysql/mysqlclient ssl z
+WANTLIB-mysql+= ${WANTLIB} iconv mariadb z

# PostgreSQL
.if ${BUILD_PACKAGES:M-pgsql}
@@ -91,7 +93,7 @@ CONFIGURE_ARGS+= --without-pg-config
LIB_DEPENDS-pgsql= ${LIB_DEPENDS} \
databases/postgresql,-main
RUN_DEPENDS-pgsql= net/powerdns
-WANTLIB-pgsql= ${WANTLIB} crypto pq>=2 ssl
+WANTLIB-pgsql= ${WANTLIB} pq>=2

# LDAP
.if ${BUILD_PACKAGES:M-ldap}
@@ -104,7 +106,7 @@ LIB_DEPENDS-ldap= ${LIB_DEPENDS} \
security/heimdal,-libs
RUN_DEPENDS-ldap= net/powerdns
WANTLIB-ldap= ${WANTLIB} ldap_r
-WANTLIB-ldap+= c com_err crypto lber-2.4 ldap_r-2.4 sasl2 ssl util
+WANTLIB-ldap+= c com_err lber sasl2 util
WANTLIB-ldap+= heimdal/lib/asn1 heimdal/lib/hcrypto heimdal/lib/heimbase
WANTLIB-ldap+= heimdal/lib/heimsqlite heimdal/lib/hx509 heimdal/lib/krb5
WANTLIB-ldap+= heimdal/lib/roken heimdal/lib/wind

Re: OpenBSD 6.6 snapshot #262 - no USB mouse

Mikal, as your problem started before the problematic snapshot, while
it may seem a similar issue, it definitely needs investigating differently.

On 2019/08/30 17:26, Mikal Villa wrote:
> I tried that, booted with #248 but I'm sorry to say the issues are still
> here. I wrote wrong in the last mail, wsmouse0 is the touchscreen which
> as last time, is no responsive. wsmouse1, the trackpad is "sometimes"
> acting on input but not nessesarry where you meant it to go, however
> right clicking seem to work, and has in all tries of mine worked.
>
> Is there a place I can read about whats already known about this issue?
> I know you don't do bugtrackers, but maybe if I knew more I could make a
> brave attempt to help fixing it myself. Unfamiliar with the openbsd
> kernel, but has a little experience from xnu and linux. Dmesg has all
> it's output from pms0, but I've read the pms driver code and I suspect
> it's not the trouble maker but something else where it's just a
> biproduct of it.

The best easy-ish thing you could do would be to try to identify a time
range (or even better the actual commit) when the problem started occurring.

The pms entries in dmesg seem to point at something kernel-side rather
than X so I would start by just trying different kernels. You could e.g.
fetch the src tree if you don't already have it, then do a date-based
update in /sys ("cvs up -Pd -D 2019/08/01"). Start with a date before
you think the problem started, to confirm that it was indeed working at
that point and to confirm that the process of just building kernels is
good enough for these tests. (If you go back too far you may run into
syscall or kernel structure incompatibilities, but I can't think of any
that will cause major problems in the suggested time window).
Build/install a kernel and test, if it works then do another cvs up
moving forward through time (forwards a week or so?) until it stops
working, then backwards again with smaller increments to narrow it down.

[Update] databases/p5-Mojo-Pg : Update to 4.15

Index: Makefile
===================================================================
RCS file: /cvs/ports/databases/p5-Mojo-Pg/Makefile,v
retrieving revision 1.6
diff -u -p -r1.6 Makefile
--- Makefile 12 Jul 2019 20:43:57 -0000 1.6
+++ Makefile 30 Aug 2019 15:37:13 -0000
@@ -4,12 +4,12 @@ COMMENT = dbd-pg wrapper for mojoliciou

MODULES = cpan databases/postgresql
PKG_ARCH = *
-DISTNAME = Mojo-Pg-4.13
+DISTNAME = Mojo-Pg-4.15
CPAN_AUTHOR = SRI
CATEGORIES = databases
MAINTAINER = Abel Abraham Camarillo Ojeda <acamari@verlet.org>

-#Perl
+# artistic 2.0
PERMIT_PACKAGE = Yes

RUN_DEPENDS = databases/p5-DBD-Pg>=3.5.1 \
@@ -18,5 +18,6 @@ RUN_DEPENDS = databases/p5-DBD-Pg>=3.5.

MODPOSTGRESQL_TEST_DBNAME = testdb
TEST_FLAGS = TEST_ONLINE=postgresql:///${MODPOSTGRESQL_TEST_DBNAME}
+MAKE_ENV = TEST_POD=yes

.include <bsd.port.mk>
Index: distinfo
===================================================================
RCS file: /cvs/ports/databases/p5-Mojo-Pg/distinfo,v
retrieving revision 1.3
diff -u -p -r1.3 distinfo
--- distinfo 5 Mar 2019 21:58:17 -0000 1.3
+++ distinfo 30 Aug 2019 15:37:13 -0000
@@ -1,2 +1,2 @@
-SHA256 (Mojo-Pg-4.13.tar.gz) = XtLcqkdCMqqUg3oFQHY9IRdt5W6WaFEut7UtApfwCKA=
-SIZE (Mojo-Pg-4.13.tar.gz) = 37795
+SHA256 (Mojo-Pg-4.15.tar.gz) = 77fp6knBJNdPOjxb+4mOdNrR7EEUB+Anj0jJJga6jLw=
+SIZE (Mojo-Pg-4.15.tar.gz) = 38104
Hi,

Here is a patch for databases/p5-Mojo-Pg:
i) Update to 4.15
ii) Fix LICENSE to artistic 2.0
iii) Add TEST_POD=yes to MAKE_ENV

It build well and passed all tests on amd64-head system.
No other ports depends on it.

Comments? OK?
wen

Re: update math/coq

On Fri, Aug 30, 2019 at 10:01:59AM +0200, Christopher Zimmermann wrote:
> Hi,
>
> I'd like to update math/coq to 8.10+beta2. Which is needed to support
> OCaml 4.08. The only user of coq is lang/compcert and was already
> updated to support Coq 8.10 and OCaml 4.08.
> When this update and the devel/frama-c update are committed the OCaml
> 4.08 update can go in. Tested on amd64 with and without nativecode. OKs?
>
> Christopher
>

Not a coq user, so I can't say if this impacts any use case. But
certainly no objections. Especially since this moves the port even
ahead of what is available in opam!

And I would love to see 4.08 make 6.6.

.... Ken

>
> Index: Makefile
> ===================================================================
> RCS file: /cvs/ports/math/coq/Makefile,v
> retrieving revision 1.40
> diff -u -p -r1.40 Makefile
> --- Makefile 12 Jul 2019 20:47:40 -0000 1.40
> +++ Makefile 30 Aug 2019 07:57:23 -0000
> @@ -2,12 +2,12 @@
>
> COMMENT= proof assistant based on a typed lambda calculus
>
> -V= 8.8.0
> +V= 8.10+beta2
> GH_ACCOUNT = coq
> GH_PROJECT = coq
> GH_TAGNAME = V${V}
> -DISTNAME = ${GH_PROJECT}-${V}
> -WRKDIST = ${WRKDIR}/${GH_PROJECT}-${V}
> +DISTNAME = ${GH_PROJECT}-${V:S/+//}
> +WRKDIST = ${WRKDIR}/${GH_PROJECT}-${V:S/+/-/}
>
> CATEGORIES= math
> HOMEPAGE= https://coq.inria.fr/
> @@ -17,27 +17,23 @@ MAINTAINER= Yozo Toda <yozo@v007.vaio.n
> # LGPL 2.1
> PERMIT_PACKAGE= Yes
>
> -WANTLIB += X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama
> -WANTLIB += Xrandr Xrender atk-1.0 c cairo fontconfig freetype fribidi
> -WANTLIB += gdk-x11-2.0 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0
> -WANTLIB += gtksourceview-2.0 gtk-x11-2.0 intl m pango-1.0 pangocairo-1.0
> -WANTLIB += pangoft2-1.0 pthread z
> +WANTLIB += atk-1.0 c cairo cairo-gobject fontconfig freetype gdk-3
> +WANTLIB += gdk_pixbuf-2.0 gio-2.0 glib-2.0 gobject-2.0 gtk-3 gtksourceview-3.0
> +WANTLIB += intl m pango-1.0 pangocairo-1.0 pthread z
>
> MODULES= lang/ocaml
>
> -BUILD_DEPENDS= x11/lablgtk2 \
> - lang/ocaml-camlp5 \
> +BUILD_DEPENDS= x11/lablgtk3 \
> math/ocaml-num \
> sysutils/findlib
> -RUN_DEPENDS= x11/lablgtk2
> +RUN_DEPENDS= x11/lablgtk3
>
> DESTDIRNAME= COQINSTALLPREFIX
>
> USE_GMAKE= Yes
>
> CONFIGURE_STYLE= simple
> -CONFIGURE_ARGS= -emacslib ${PREFIX}/share/emacs/site-lisp \
> - -prefix ${PREFIX} \
> +CONFIGURE_ARGS= -prefix ${PREFIX} \
> -libdir ${PREFIX}/lib/ocaml/coq \
> -mandir ${PREFIX}/man \
> -configdir ${SYSCONFDIR}/xdg/coq
> @@ -65,7 +61,7 @@ post-install:
> ${INSTALL_DATA_DIR} \
> ${PREFIX}/share/doc/coq/
> ${INSTALL_DATA} \
> - ${WRKDIST}/{LICENSE,CREDITS,CHANGES,CONTRIBUTING.md,README.md} \
> + ${WRKDIST}/{LICENSE,CREDITS,CONTRIBUTING.md,README.md} \
> ${PREFIX}/share/doc/coq/
>
> .include <bsd.port.mk>
> Index: distinfo
> ===================================================================
> RCS file: /cvs/ports/math/coq/distinfo,v
> retrieving revision 1.14
> diff -u -p -r1.14 distinfo
> --- distinfo 4 Mar 2019 12:51:15 -0000 1.14
> +++ distinfo 30 Aug 2019 07:57:23 -0000
> @@ -1,2 +1,2 @@
> -SHA256 (coq-8.8.0.tar.gz) = yvfB055o4OQe2Svh1XyImD+xLtufqVZnpa0tarqYJj0=
> -SIZE (coq-8.8.0.tar.gz) = 5927663
> +SHA256 (coq-8.10beta2.tar.gz) = LIK7Tew3o/+lfuDWQm8OfezMbLM0AA2+Z7DNUV2FUBY=
> +SIZE (coq-8.10beta2.tar.gz) = 6211659
> Index: patches/patch-Makefile_ide
> ===================================================================
> RCS file: /cvs/ports/math/coq/patches/patch-Makefile_ide,v
> retrieving revision 1.1
> diff -u -p -r1.1 patch-Makefile_ide
> --- patches/patch-Makefile_ide 4 Mar 2019 12:51:15 -0000 1.1
> +++ patches/patch-Makefile_ide 30 Aug 2019 07:57:23 -0000
> @@ -3,7 +3,7 @@ $OpenBSD: patch-Makefile_ide,v 1.1 2019/
> Index: Makefile.ide
> --- Makefile.ide.orig
> +++ Makefile.ide
> -@@ -149,7 +149,7 @@ endif
> +@@ -190,7 +190,7 @@ endif
> ifeq ($(HASCOQIDE),no)
> install-coqide-byte: install-ide-toploop-byte
> else
> Index: patches/patch-Makefile_install
> ===================================================================
> RCS file: patches/patch-Makefile_install
> diff -N patches/patch-Makefile_install
> --- patches/patch-Makefile_install 4 Mar 2019 12:51:15 -0000 1.1
> +++ /dev/null 1 Jan 1970 00:00:00 -0000
> @@ -1,19 +0,0 @@
> -$OpenBSD: patch-Makefile_install,v 1.1 2019/03/04 12:51:15 chrisz Exp $
> -
> -Index: Makefile.install
> ---- Makefile.install.orig
> -+++ Makefile.install
> -@@ -110,11 +110,11 @@ install-devfiles:
> - $(MKDIR) $(FULLCOQLIB)
> - $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA)
> - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files
> -+ $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS)
> -+ifeq ($(BEST),opt)
> - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning 58 "-opaque"
> - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
> - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o) # For static linking of plugins
> -- $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS)
> --ifeq ($(BEST),opt)
> - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
> - endif
> -
> Index: patches/patch-configure_ml
> ===================================================================
> RCS file: /cvs/ports/math/coq/patches/patch-configure_ml,v
> retrieving revision 1.1
> diff -u -p -r1.1 patch-configure_ml
> --- patches/patch-configure_ml 4 Mar 2019 12:51:15 -0000 1.1
> +++ patches/patch-configure_ml 30 Aug 2019 07:57:23 -0000
> @@ -5,7 +5,7 @@ those ticks seem to prevent proper parsi
> Index: configure.ml
> --- configure.ml.orig
> +++ configure.ml
> -@@ -1077,7 +1077,7 @@ let config_runtime () =
> +@@ -940,7 +940,7 @@ let config_runtime () =
> ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"]
> | _ ->
> let ld="CAML_LD_LIBRARY_PATH" in
> Index: pkg/PFRAG.dynlink-native
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
> retrieving revision 1.4
> diff -u -p -r1.4 PFRAG.dynlink-native
> --- pkg/PFRAG.dynlink-native 4 Mar 2019 12:51:15 -0000 1.4
> +++ pkg/PFRAG.dynlink-native 30 Aug 2019 07:57:23 -0000
> @@ -25,17 +25,17 @@
> @bin lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
> @bin lib/ocaml/coq/plugins/extraction/extraction_plugin.cmxs
> @bin lib/ocaml/coq/plugins/firstorder/ground_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmxs
> -@bin lib/ocaml/coq/plugins/fourier/fourier_plugin.cmxs
> @bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmxs
> @bin lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmxs
> @bin lib/ocaml/coq/plugins/funind/recdef_plugin.cmxs
> @bin lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmxs
> @bin lib/ocaml/coq/plugins/ltac/ltac_plugin.cmxs
> @bin lib/ocaml/coq/plugins/ltac/tauto_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
> +@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmxs
> +@bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmxs
> @bin lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
> @@ -59,11 +59,6 @@
> @bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmxs
> @bin lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmxs
> @bin lib/ocaml/coq/plugins/omega/omega_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmxs
> -@bin lib/ocaml/coq/plugins/quote/quote_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmxs
> -@bin lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmxs
> -@bin lib/ocaml/coq/plugins/romega/romega_plugin.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmxs
> @bin lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmxs
> @@ -98,12 +93,10 @@
> @bin lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmxs
> @bin lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
> @bin lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmxs
> @bin lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmxs
> -@bin lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmxs
> +@bin lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.cmxs
> @bin lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Between.cmxs
> @@ -149,9 +142,9 @@
> @bin lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidDec.cmxs
> @bin lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.cmxs
> @bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
> -@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmxs
> -@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmxs
> +@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmxs
> @bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmxs
> +@bin lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFullAVL.cmxs
> @@ -173,6 +166,7 @@
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetToFiniteSet.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmxs
> @bin lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmxs
> +@bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmxs
> @bin lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmxs
> @@ -226,6 +220,7 @@
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmxs
> +@bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmxs
> @bin lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmxs
> @bin lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetAVL.cmxs
> @@ -251,6 +246,7 @@
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ngcd_def.cmxs
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.cmxs
> @bin lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmxs
> +@bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmxs
> @bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmxs
> @bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmxs
> @bin lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmxs
> @@ -266,6 +262,9 @@
> @bin lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmxs
> @bin lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.cmxs
> @bin lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmxs
> +@bin lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmxs
> +@bin lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmxs
> +@bin lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmxs
> @bin lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmxs
> @bin lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmxs
> @bin lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAddOrder.cmxs
> @@ -409,6 +408,7 @@
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmxs
> +@bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmxs
> @bin lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmxs
> @@ -449,6 +449,11 @@
> @bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorted.cmxs
> @bin lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.cmxs
> @bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmxs
> +@bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmxs
> @bin lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmxs
> @bin lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmxs
> @bin lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableTypeEx.cmxs
> @@ -513,7 +518,3 @@
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zsqrt_compat.cmxs
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmxs
> @bin lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmxs
> -@bin lib/ocaml/coq/toploop/coqidetop.cmxs
> -@bin lib/ocaml/coq/toploop/proofworkertop.cmxs
> -@bin lib/ocaml/coq/toploop/queryworkertop.cmxs
> -@bin lib/ocaml/coq/toploop/tacworkertop.cmxs
> Index: pkg/PFRAG.native
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PFRAG.native,v
> retrieving revision 1.3
> diff -u -p -r1.3 PFRAG.native
> --- pkg/PFRAG.native 4 Mar 2019 12:51:15 -0000 1.3
> +++ pkg/PFRAG.native 30 Aug 2019 07:57:24 -0000
> @@ -1,5 +1,10 @@
> @comment $OpenBSD: PFRAG.native,v 1.3 2019/03/04 12:51:15 chrisz Exp $
> %%dynlink%%
> +@bin bin/coqidetop.opt
> +@bin bin/coqproofworker.opt
> +@bin bin/coqqueryworker.opt
> +@bin bin/coqtacticworker.opt
> +@bin bin/coqtop.opt
> lib/ocaml/coq/clib/backtrace.cmx
> lib/ocaml/coq/clib/bigint.cmx
> lib/ocaml/coq/clib/cArray.cmx
> @@ -12,9 +17,9 @@ lib/ocaml/coq/clib/cStack.cmx
> lib/ocaml/coq/clib/cString.cmx
> lib/ocaml/coq/clib/cThread.cmx
> lib/ocaml/coq/clib/cUnix.cmx
> -lib/ocaml/coq/clib/canary.cmx
> lib/ocaml/coq/clib/clib.a
> lib/ocaml/coq/clib/clib.cmxa
> +lib/ocaml/coq/clib/diff2.cmx
> lib/ocaml/coq/clib/dyn.cmx
> lib/ocaml/coq/clib/exninfo.cmx
> lib/ocaml/coq/clib/hMap.cmx
> @@ -36,10 +41,13 @@ lib/ocaml/coq/clib/trie.cmx
> lib/ocaml/coq/clib/unicode.cmx
> lib/ocaml/coq/clib/unicodetable.cmx
> lib/ocaml/coq/clib/unionfind.cmx
> +lib/ocaml/coq/config/config.a
> +lib/ocaml/coq/config/config.cmxa
> lib/ocaml/coq/config/coq_config.cmx
> lib/ocaml/coq/engine/eConstr.cmx
> lib/ocaml/coq/engine/engine.a
> lib/ocaml/coq/engine/engine.cmxa
> +lib/ocaml/coq/engine/evar_kinds.cmx
> lib/ocaml/coq/engine/evarutil.cmx
> lib/ocaml/coq/engine/evd.cmx
> lib/ocaml/coq/engine/ftactic.cmx
> @@ -50,10 +58,21 @@ lib/ocaml/coq/engine/proofview.cmx
> lib/ocaml/coq/engine/proofview_monad.cmx
> lib/ocaml/coq/engine/termops.cmx
> lib/ocaml/coq/engine/uState.cmx
> -lib/ocaml/coq/engine/universes.cmx
> +lib/ocaml/coq/engine/univGen.cmx
> +lib/ocaml/coq/engine/univMinim.cmx
> +lib/ocaml/coq/engine/univNames.cmx
> +lib/ocaml/coq/engine/univProblem.cmx
> +lib/ocaml/coq/engine/univSubst.cmx
> lib/ocaml/coq/engine/univops.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib.a
> +lib/ocaml/coq/gramlib/.pack/gramlib.cmxa
> +lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Plexing.cmx
> +lib/ocaml/coq/gramlib/.pack/gramlib__Ploc.cmx
> lib/ocaml/coq/ide/ide.a
> lib/ocaml/coq/ide/ide.cmxa
> +lib/ocaml/coq/interp/constrexpr.cmx
> lib/ocaml/coq/interp/constrexpr_ops.cmx
> lib/ocaml/coq/interp/constrextern.cmx
> lib/ocaml/coq/interp/constrintern.cmx
> @@ -68,26 +87,12 @@ lib/ocaml/coq/interp/interp.cmxa
> lib/ocaml/coq/interp/modintern.cmx
> lib/ocaml/coq/interp/notation.cmx
> lib/ocaml/coq/interp/notation_ops.cmx
> -lib/ocaml/coq/interp/ppextend.cmx
> +lib/ocaml/coq/interp/notation_term.cmx
> +lib/ocaml/coq/interp/numTok.cmx
> lib/ocaml/coq/interp/reserve.cmx
> lib/ocaml/coq/interp/smartlocate.cmx
> lib/ocaml/coq/interp/stdarg.cmx
> lib/ocaml/coq/interp/syntax_def.cmx
> -lib/ocaml/coq/interp/tactypes.cmx
> -lib/ocaml/coq/interp/topconstr.cmx
> -lib/ocaml/coq/intf/constrexpr.cmx
> -lib/ocaml/coq/intf/decl_kinds.cmx
> -lib/ocaml/coq/intf/evar_kinds.cmx
> -lib/ocaml/coq/intf/extend.cmx
> -lib/ocaml/coq/intf/genredexpr.cmx
> -lib/ocaml/coq/intf/glob_term.cmx
> -lib/ocaml/coq/intf/intf.a
> -lib/ocaml/coq/intf/intf.cmxa
> -lib/ocaml/coq/intf/locus.cmx
> -lib/ocaml/coq/intf/misctypes.cmx
> -lib/ocaml/coq/intf/notation_term.cmx
> -lib/ocaml/coq/intf/pattern.cmx
> -lib/ocaml/coq/intf/vernacexpr.cmx
> lib/ocaml/coq/kernel/cClosure.cmx
> lib/ocaml/coq/kernel/cPrimitives.cmx
> lib/ocaml/coq/kernel/cbytecodes.cmx
> @@ -106,6 +111,7 @@ lib/ocaml/coq/kernel/entries.cmx
> lib/ocaml/coq/kernel/environ.cmx
> lib/ocaml/coq/kernel/esubst.cmx
> lib/ocaml/coq/kernel/evar.cmx
> +lib/ocaml/coq/kernel/indTyping.cmx
> lib/ocaml/coq/kernel/indtypes.cmx
> lib/ocaml/coq/kernel/inductive.cmx
> lib/ocaml/coq/kernel/kernel.a
> @@ -121,23 +127,26 @@ lib/ocaml/coq/kernel/nativelib.cmx
> lib/ocaml/coq/kernel/nativelibrary.cmx
> lib/ocaml/coq/kernel/nativevalues.cmx
> lib/ocaml/coq/kernel/opaqueproof.cmx
> -lib/ocaml/coq/kernel/pre_env.cmx
> +lib/ocaml/coq/kernel/primred.cmx
> lib/ocaml/coq/kernel/reduction.cmx
> lib/ocaml/coq/kernel/retroknowledge.cmx
> +lib/ocaml/coq/kernel/retypeops.cmx
> lib/ocaml/coq/kernel/safe_typing.cmx
> lib/ocaml/coq/kernel/sorts.cmx
> lib/ocaml/coq/kernel/subtyping.cmx
> lib/ocaml/coq/kernel/term.cmx
> lib/ocaml/coq/kernel/term_typing.cmx
> +lib/ocaml/coq/kernel/transparentState.cmx
> lib/ocaml/coq/kernel/type_errors.cmx
> lib/ocaml/coq/kernel/typeops.cmx
> lib/ocaml/coq/kernel/uGraph.cmx
> -lib/ocaml/coq/kernel/uint31.cmx
> +lib/ocaml/coq/kernel/uint63.cmx
> lib/ocaml/coq/kernel/univ.cmx
> lib/ocaml/coq/kernel/vars.cmx
> lib/ocaml/coq/kernel/vconv.cmx
> lib/ocaml/coq/kernel/vm.cmx
> lib/ocaml/coq/kernel/vmvalues.cmx
> +lib/ocaml/coq/lib/acyclicGraph.cmx
> lib/ocaml/coq/lib/aux_file.cmx
> lib/ocaml/coq/lib/cAst.cmx
> lib/ocaml/coq/lib/cErrors.cmx
> @@ -157,6 +166,7 @@ lib/ocaml/coq/lib/lib.a
> lib/ocaml/coq/lib/lib.cmxa
> lib/ocaml/coq/lib/loc.cmx
> lib/ocaml/coq/lib/pp.cmx
> +lib/ocaml/coq/lib/pp_diff.cmx
> lib/ocaml/coq/lib/remoteCounter.cmx
> lib/ocaml/coq/lib/rtree.cmx
> lib/ocaml/coq/lib/spawn.cmx
> @@ -164,13 +174,12 @@ lib/ocaml/coq/lib/stateid.cmx
> lib/ocaml/coq/lib/system.cmx
> lib/ocaml/coq/lib/util.cmx
> lib/ocaml/coq/library/coqlib.cmx
> +lib/ocaml/coq/library/decl_kinds.cmx
> lib/ocaml/coq/library/declaremods.cmx
> lib/ocaml/coq/library/decls.cmx
> -lib/ocaml/coq/library/dischargedhypsmap.cmx
> lib/ocaml/coq/library/global.cmx
> lib/ocaml/coq/library/globnames.cmx
> lib/ocaml/coq/library/goptions.cmx
> -lib/ocaml/coq/library/heads.cmx
> lib/ocaml/coq/library/keys.cmx
> lib/ocaml/coq/library/kindops.cmx
> lib/ocaml/coq/library/lib.cmx
> @@ -184,15 +193,15 @@ lib/ocaml/coq/library/nametab.cmx
> lib/ocaml/coq/library/states.cmx
> lib/ocaml/coq/library/summary.cmx
> lib/ocaml/coq/parsing/cLexer.cmx
> -lib/ocaml/coq/parsing/egramcoq.cmx
> -lib/ocaml/coq/parsing/egramml.cmx
> +lib/ocaml/coq/parsing/extend.cmx
> lib/ocaml/coq/parsing/g_constr.cmx
> lib/ocaml/coq/parsing/g_prim.cmx
> -lib/ocaml/coq/parsing/g_proofs.cmx
> -lib/ocaml/coq/parsing/g_vernac.cmx
> +lib/ocaml/coq/parsing/notation_gram.cmx
> +lib/ocaml/coq/parsing/notgram_ops.cmx
> lib/ocaml/coq/parsing/parsing.a
> lib/ocaml/coq/parsing/parsing.cmxa
> lib/ocaml/coq/parsing/pcoq.cmx
> +lib/ocaml/coq/parsing/ppextend.cmx
> lib/ocaml/coq/parsing/tok.cmx
> lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
> lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
> @@ -273,15 +282,6 @@ lib/ocaml/coq/plugins/firstorder/instanc
> lib/ocaml/coq/plugins/firstorder/rules.cmx
> lib/ocaml/coq/plugins/firstorder/sequent.cmx
> lib/ocaml/coq/plugins/firstorder/unify.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.o
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmx
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.o
> -lib/ocaml/coq/plugins/fourier/fourier.cmx
> -lib/ocaml/coq/plugins/fourier/fourierR.cmx
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.cmx
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.o
> -lib/ocaml/coq/plugins/fourier/g_fourier.cmx
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmx
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.o
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
> @@ -331,10 +331,16 @@ lib/ocaml/coq/plugins/ltac/tactic_option
> lib/ocaml/coq/plugins/ltac/tauto.cmx
> lib/ocaml/coq/plugins/ltac/tauto_plugin.cmx
> lib/ocaml/coq/plugins/ltac/tauto_plugin.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.o
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmx
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmx
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.o
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmx
> @@ -367,6 +373,7 @@ lib/ocaml/coq/plugins/micromega/certific
> lib/ocaml/coq/plugins/micromega/coq_micromega.cmx
> lib/ocaml/coq/plugins/micromega/csdpcert.cmx
> lib/ocaml/coq/plugins/micromega/g_micromega.cmx
> +lib/ocaml/coq/plugins/micromega/itv.cmx
> lib/ocaml/coq/plugins/micromega/mfourier.cmx
> lib/ocaml/coq/plugins/micromega/micromega.cmx
> lib/ocaml/coq/plugins/micromega/micromega_plugin.cmx
> @@ -374,9 +381,11 @@ lib/ocaml/coq/plugins/micromega/micromeg
> lib/ocaml/coq/plugins/micromega/mutils.cmx
> lib/ocaml/coq/plugins/micromega/persistent_cache.cmx
> lib/ocaml/coq/plugins/micromega/polynomial.cmx
> +lib/ocaml/coq/plugins/micromega/simplex.cmx
> lib/ocaml/coq/plugins/micromega/sos.cmx
> lib/ocaml/coq/plugins/micromega/sos_lib.cmx
> lib/ocaml/coq/plugins/micromega/sos_types.cmx
> +lib/ocaml/coq/plugins/micromega/vect.cmx
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.o
> lib/ocaml/coq/plugins/nsatz/g_nsatz.cmx
> @@ -401,21 +410,6 @@ lib/ocaml/coq/plugins/omega/g_omega.cmx
> lib/ocaml/coq/plugins/omega/omega.cmx
> lib/ocaml/coq/plugins/omega/omega_plugin.cmx
> lib/ocaml/coq/plugins/omega/omega_plugin.o
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.o
> -lib/ocaml/coq/plugins/quote/g_quote.cmx
> -lib/ocaml/coq/plugins/quote/quote.cmx
> -lib/ocaml/coq/plugins/quote/quote_plugin.cmx
> -lib/ocaml/coq/plugins/quote/quote_plugin.o
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.o
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmx
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.o
> -lib/ocaml/coq/plugins/romega/const_omega.cmx
> -lib/ocaml/coq/plugins/romega/g_romega.cmx
> -lib/ocaml/coq/plugins/romega/refl_omega.cmx
> -lib/ocaml/coq/plugins/romega/romega_plugin.cmx
> -lib/ocaml/coq/plugins/romega/romega_plugin.o
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.o
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmx
> @@ -499,27 +493,24 @@ lib/ocaml/coq/plugins/ssr/ssrvernac.cmx
> lib/ocaml/coq/plugins/ssr/ssrview.cmx
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
> +lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmx
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.o
> -lib/ocaml/coq/plugins/syntax/ascii_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/int31_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/nat_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/g_numeral.cmx
> +lib/ocaml/coq/plugins/syntax/g_string.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/numeral.cmx
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.o
> lib/ocaml/coq/plugins/syntax/r_syntax.cmx
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmx
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/string_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.o
> -lib/ocaml/coq/plugins/syntax/z_syntax.cmx
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmx
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.o
> +lib/ocaml/coq/plugins/syntax/string_notation.cmx
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmx
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.o
> lib/ocaml/coq/pretyping/arguments_renaming.cmx
> lib/ocaml/coq/pretyping/cases.cmx
> lib/ocaml/coq/pretyping/cbv.cmx
> @@ -532,14 +523,18 @@ lib/ocaml/coq/pretyping/evardefine.cmx
> lib/ocaml/coq/pretyping/evarsolve.cmx
> lib/ocaml/coq/pretyping/find_subterm.cmx
> lib/ocaml/coq/pretyping/geninterp.cmx
> +lib/ocaml/coq/pretyping/globEnv.cmx
> lib/ocaml/coq/pretyping/glob_ops.cmx
> +lib/ocaml/coq/pretyping/glob_term.cmx
> +lib/ocaml/coq/pretyping/heads.cmx
> lib/ocaml/coq/pretyping/indrec.cmx
> lib/ocaml/coq/pretyping/inductiveops.cmx
> lib/ocaml/coq/pretyping/inferCumulativity.cmx
> +lib/ocaml/coq/pretyping/locus.cmx
> lib/ocaml/coq/pretyping/locusops.cmx
> lib/ocaml/coq/pretyping/ltac_pretype.cmx
> -lib/ocaml/coq/pretyping/miscops.cmx
> lib/ocaml/coq/pretyping/nativenorm.cmx
> +lib/ocaml/coq/pretyping/pattern.cmx
> lib/ocaml/coq/pretyping/patternops.cmx
> lib/ocaml/coq/pretyping/pretype_errors.cmx
> lib/ocaml/coq/pretyping/pretyping.a
> @@ -547,7 +542,6 @@ lib/ocaml/coq/pretyping/pretyping.cmx
> lib/ocaml/coq/pretyping/pretyping.cmxa
> lib/ocaml/coq/pretyping/program.cmx
> lib/ocaml/coq/pretyping/recordops.cmx
> -lib/ocaml/coq/pretyping/redops.cmx
> lib/ocaml/coq/pretyping/reductionops.cmx
> lib/ocaml/coq/pretyping/retyping.cmx
> lib/ocaml/coq/pretyping/tacred.cmx
> @@ -555,51 +549,47 @@ lib/ocaml/coq/pretyping/typeclasses.cmx
> lib/ocaml/coq/pretyping/typeclasses_errors.cmx
> lib/ocaml/coq/pretyping/typing.cmx
> lib/ocaml/coq/pretyping/unification.cmx
> -lib/ocaml/coq/pretyping/univdecls.cmx
> lib/ocaml/coq/pretyping/vnorm.cmx
> lib/ocaml/coq/printing/genprint.cmx
> lib/ocaml/coq/printing/ppconstr.cmx
> lib/ocaml/coq/printing/pputils.cmx
> -lib/ocaml/coq/printing/ppvernac.cmx
> lib/ocaml/coq/printing/prettyp.cmx
> lib/ocaml/coq/printing/printer.cmx
> lib/ocaml/coq/printing/printing.a
> lib/ocaml/coq/printing/printing.cmxa
> lib/ocaml/coq/printing/printmod.cmx
> +lib/ocaml/coq/printing/proof_diffs.cmx
> lib/ocaml/coq/proofs/clenv.cmx
> lib/ocaml/coq/proofs/clenvtac.cmx
> lib/ocaml/coq/proofs/evar_refiner.cmx
> lib/ocaml/coq/proofs/goal.cmx
> +lib/ocaml/coq/proofs/goal_select.cmx
> lib/ocaml/coq/proofs/logic.cmx
> lib/ocaml/coq/proofs/miscprint.cmx
> lib/ocaml/coq/proofs/pfedit.cmx
> lib/ocaml/coq/proofs/proof.cmx
> lib/ocaml/coq/proofs/proof_bullet.cmx
> lib/ocaml/coq/proofs/proof_global.cmx
> -lib/ocaml/coq/proofs/proof_type.cmx
> lib/ocaml/coq/proofs/proofs.a
> lib/ocaml/coq/proofs/proofs.cmxa
> -lib/ocaml/coq/proofs/redexpr.cmx
> lib/ocaml/coq/proofs/refine.cmx
> lib/ocaml/coq/proofs/refiner.cmx
> lib/ocaml/coq/proofs/tacmach.cmx
> +lib/ocaml/coq/proofs/tactypes.cmx
> lib/ocaml/coq/stm/asyncTaskQueue.cmx
> lib/ocaml/coq/stm/coqworkmgrApi.cmx
> lib/ocaml/coq/stm/dag.cmx
> lib/ocaml/coq/stm/proofBlockDelimiter.cmx
> -lib/ocaml/coq/stm/proofworkertop.cmx
> -lib/ocaml/coq/stm/queryworkertop.cmx
> lib/ocaml/coq/stm/spawned.cmx
> lib/ocaml/coq/stm/stm.a
> lib/ocaml/coq/stm/stm.cmx
> lib/ocaml/coq/stm/stm.cmxa
> lib/ocaml/coq/stm/tQueue.cmx
> -lib/ocaml/coq/stm/tacworkertop.cmx
> lib/ocaml/coq/stm/vcs.cmx
> lib/ocaml/coq/stm/vernac_classifier.cmx
> lib/ocaml/coq/stm/vio_checking.cmx
> -lib/ocaml/coq/stm/workerLoop.cmx
> lib/ocaml/coq/stm/workerPool.cmx
> +lib/ocaml/coq/tactics/abstract.cmx
> lib/ocaml/coq/tactics/auto.cmx
> lib/ocaml/coq/tactics/autorewrite.cmx
> lib/ocaml/coq/tactics/btermdn.cmx
> @@ -613,11 +603,15 @@ lib/ocaml/coq/tactics/elimschemes.cmx
> lib/ocaml/coq/tactics/eqdecide.cmx
> lib/ocaml/coq/tactics/eqschemes.cmx
> lib/ocaml/coq/tactics/equality.cmx
> +lib/ocaml/coq/tactics/genredexpr.cmx
> lib/ocaml/coq/tactics/hints.cmx
> lib/ocaml/coq/tactics/hipattern.cmx
> lib/ocaml/coq/tactics/ind_tables.cmx
> lib/ocaml/coq/tactics/inv.cmx
> lib/ocaml/coq/tactics/leminv.cmx
> +lib/ocaml/coq/tactics/ppred.cmx
> +lib/ocaml/coq/tactics/redexpr.cmx
> +lib/ocaml/coq/tactics/redops.cmx
> lib/ocaml/coq/tactics/tacticals.cmx
> lib/ocaml/coq/tactics/tactics.a
> lib/ocaml/coq/tactics/tactics.cmx
> @@ -713,12 +707,12 @@ lib/ocaml/coq/theories/Classes/.coq-nati
> lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.o
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmx
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.o
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmx
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.o
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmx
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.o
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmx
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.o
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmx
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmx
> @@ -761,6 +755,8 @@ lib/ocaml/coq/theories/FSets/.coq-native
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.o
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmx
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.o
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmx
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.o
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmx
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.o
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmx
> @@ -867,6 +863,8 @@ lib/ocaml/coq/theories/Logic/.coq-native
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmx
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.o
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmx
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmx
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.o
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmx
> @@ -917,6 +915,8 @@ lib/ocaml/coq/theories/NArith/.coq-nativ
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.o
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmx
> lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.o
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmx
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.o
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmx
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.o
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmx
> @@ -947,6 +947,12 @@ lib/ocaml/coq/theories/Numbers/Cyclic/In
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.o
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmx
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.o
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmx
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.o
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmx
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.o
> lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmx
> @@ -1233,6 +1239,8 @@ lib/ocaml/coq/theories/Reals/.coq-native
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmx
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.o
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmx
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmx
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.o
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmx
> @@ -1313,6 +1321,16 @@ lib/ocaml/coq/theories/Sorting/.coq-nati
> lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.o
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmx
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.o
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmx
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.o
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmx
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.o
> lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmx
> @@ -1441,16 +1459,26 @@ lib/ocaml/coq/theories/ZArith/.coq-nativ
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
> lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
> +lib/ocaml/coq/topbin/coqc_bin.cmx
> +lib/ocaml/coq/topbin/coqproofworker_bin.cmx
> +lib/ocaml/coq/topbin/coqqueryworker_bin.cmx
> +lib/ocaml/coq/topbin/coqtacticworker_bin.cmx
> +lib/ocaml/coq/topbin/coqtop_bin.cmx
> +lib/ocaml/coq/toplevel/ccompile.cmx
> lib/ocaml/coq/toplevel/coqargs.cmx
> +lib/ocaml/coq/toplevel/coqc.cmx
> +lib/ocaml/coq/toplevel/coqcargs.cmx
> lib/ocaml/coq/toplevel/coqinit.cmx
> lib/ocaml/coq/toplevel/coqloop.cmx
> lib/ocaml/coq/toplevel/coqtop.cmx
> -lib/ocaml/coq/toplevel/coqtop_opt_bin.cmx
> +lib/ocaml/coq/toplevel/g_toplevel.cmx
> lib/ocaml/coq/toplevel/toplevel.a
> lib/ocaml/coq/toplevel/toplevel.cmxa
> lib/ocaml/coq/toplevel/usage.cmx
> lib/ocaml/coq/toplevel/vernac.cmx
> +lib/ocaml/coq/toplevel/workerLoop.cmx
> lib/ocaml/coq/vernac/assumptions.cmx
> +lib/ocaml/coq/vernac/attributes.cmx
> lib/ocaml/coq/vernac/auto_ind_decl.cmx
> lib/ocaml/coq/vernac/class.cmx
> lib/ocaml/coq/vernac/classes.cmx
> @@ -1460,7 +1488,11 @@ lib/ocaml/coq/vernac/comFixpoint.cmx
> lib/ocaml/coq/vernac/comInductive.cmx
> lib/ocaml/coq/vernac/comProgramFixpoint.cmx
> lib/ocaml/coq/vernac/declareDef.cmx
> +lib/ocaml/coq/vernac/egramcoq.cmx
> +lib/ocaml/coq/vernac/egramml.cmx
> lib/ocaml/coq/vernac/explainErr.cmx
> +lib/ocaml/coq/vernac/g_proofs.cmx
> +lib/ocaml/coq/vernac/g_vernac.cmx
> lib/ocaml/coq/vernac/himsg.cmx
> lib/ocaml/coq/vernac/indschemes.cmx
> lib/ocaml/coq/vernac/lemmas.cmx
> @@ -1468,13 +1500,16 @@ lib/ocaml/coq/vernac/locality.cmx
> lib/ocaml/coq/vernac/metasyntax.cmx
> lib/ocaml/coq/vernac/mltop.cmx
> lib/ocaml/coq/vernac/obligations.cmx
> +lib/ocaml/coq/vernac/ppvernac.cmx
> lib/ocaml/coq/vernac/proof_using.cmx
> +lib/ocaml/coq/vernac/pvernac.cmx
> lib/ocaml/coq/vernac/record.cmx
> lib/ocaml/coq/vernac/search.cmx
> lib/ocaml/coq/vernac/topfmt.cmx
> lib/ocaml/coq/vernac/vernac.a
> lib/ocaml/coq/vernac/vernac.cmxa
> lib/ocaml/coq/vernac/vernacentries.cmx
> -lib/ocaml/coq/vernac/vernacinterp.cmx
> +lib/ocaml/coq/vernac/vernacexpr.cmx
> +lib/ocaml/coq/vernac/vernacextend.cmx
> lib/ocaml/coq/vernac/vernacprop.cmx
> lib/ocaml/coq/vernac/vernacstate.cmx
> Index: pkg/PLIST
> ===================================================================
> RCS file: /cvs/ports/math/coq/pkg/PLIST,v
> retrieving revision 1.11
> diff -u -p -r1.11 PLIST
> --- pkg/PLIST 4 Mar 2019 12:51:15 -0000 1.11
> +++ pkg/PLIST 30 Aug 2019 07:57:24 -0000
> @@ -7,11 +7,12 @@
> @bin bin/coqdep
> @bin bin/coqdoc
> @bin bin/coqide
> +@bin bin/coqidetop
> +bin/coqpp
> @bin bin/coqtop
> @comment bin/coqtop.byte
> @bin bin/coqwc
> @bin bin/coqworkmgr
> -@bin bin/gallina
> lib/ocaml/coq/
> lib/ocaml/coq/META
> lib/ocaml/coq/clib/
> @@ -28,7 +29,7 @@ lib/ocaml/coq/clib/cStack.cmi
> lib/ocaml/coq/clib/cString.cmi
> lib/ocaml/coq/clib/cThread.cmi
> lib/ocaml/coq/clib/cUnix.cmi
> -lib/ocaml/coq/clib/canary.cmi
> +lib/ocaml/coq/clib/diff2.cmi
> lib/ocaml/coq/clib/dyn.cmi
> lib/ocaml/coq/clib/exninfo.cmi
> lib/ocaml/coq/clib/hMap.cmi
> @@ -52,10 +53,14 @@ lib/ocaml/coq/clib/unicodetable.cmi
> lib/ocaml/coq/clib/unionfind.cmi
> lib/ocaml/coq/config/
> lib/ocaml/coq/config/coq_config.cmi
> +lib/ocaml/coq/coqpp/
> +lib/ocaml/coq/coqpp/coqpp_ast.cmi
> +lib/ocaml/coq/coqpp/coqpp_parse.cmi
> lib/ocaml/coq/dev/
> @comment lib/ocaml/coq/dllcoqrun.so
> lib/ocaml/coq/engine/
> lib/ocaml/coq/engine/eConstr.cmi
> +lib/ocaml/coq/engine/evar_kinds.cmi
> lib/ocaml/coq/engine/evarutil.cmi
> lib/ocaml/coq/engine/evd.cmi
> lib/ocaml/coq/engine/ftactic.cmi
> @@ -66,13 +71,24 @@ lib/ocaml/coq/engine/proofview.cmi
> lib/ocaml/coq/engine/proofview_monad.cmi
> lib/ocaml/coq/engine/termops.cmi
> lib/ocaml/coq/engine/uState.cmi
> -lib/ocaml/coq/engine/universes.cmi
> +lib/ocaml/coq/engine/univGen.cmi
> +lib/ocaml/coq/engine/univMinim.cmi
> +lib/ocaml/coq/engine/univNames.cmi
> +lib/ocaml/coq/engine/univProblem.cmi
> +lib/ocaml/coq/engine/univSubst.cmi
> lib/ocaml/coq/engine/univops.cmi
> -lib/ocaml/coq/grammar/
> -lib/ocaml/coq/grammar/grammar.cma
> -lib/ocaml/coq/grammar/q_util.cmi
> +lib/ocaml/coq/gramlib/
> +lib/ocaml/coq/gramlib/.pack/
> +lib/ocaml/coq/gramlib/.pack/gramlib.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Gramext.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Grammar.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Plexing.cmi
> +lib/ocaml/coq/gramlib/.pack/gramlib__Ploc.cmi
> lib/ocaml/coq/ide/
> lib/ocaml/coq/ide/config_lexer.cmi
> +lib/ocaml/coq/ide/configwin.cmi
> +lib/ocaml/coq/ide/configwin_ihm.cmi
> +lib/ocaml/coq/ide/configwin_messages.cmi
> lib/ocaml/coq/ide/coq.cmi
> lib/ocaml/coq/ide/coqOps.cmi
> lib/ocaml/coq/ide/coq_commands.cmi
> @@ -83,19 +99,14 @@ lib/ocaml/coq/ide/document.cmi
> lib/ocaml/coq/ide/fileOps.cmi
> lib/ocaml/coq/ide/gtk_parsing.cmi
> lib/ocaml/coq/ide/ideutils.cmi
> +lib/ocaml/coq/ide/microPG.cmi
> lib/ocaml/coq/ide/minilib.cmi
> -lib/ocaml/coq/ide/nanoPG.cmi
> lib/ocaml/coq/ide/preferences.cmi
> -lib/ocaml/coq/ide/richpp.cmi
> lib/ocaml/coq/ide/sentence.cmi
> -lib/ocaml/coq/ide/serialize.cmi
> lib/ocaml/coq/ide/session.cmi
> lib/ocaml/coq/ide/tags.cmi
> +lib/ocaml/coq/ide/unicode_bindings.cmi
> lib/ocaml/coq/ide/utf8_convert.cmi
> -lib/ocaml/coq/ide/utils/
> -lib/ocaml/coq/ide/utils/configwin.cmi
> -lib/ocaml/coq/ide/utils/configwin_ihm.cmi
> -lib/ocaml/coq/ide/utils/configwin_messages.cmi
> lib/ocaml/coq/ide/wg_Command.cmi
> lib/ocaml/coq/ide/wg_Completion.cmi
> lib/ocaml/coq/ide/wg_Detachable.cmi
> @@ -106,11 +117,8 @@ lib/ocaml/coq/ide/wg_ProofView.cmi
> lib/ocaml/coq/ide/wg_RoutedMessageViews.cmi
> lib/ocaml/coq/ide/wg_ScriptView.cmi
> lib/ocaml/coq/ide/wg_Segment.cmi
> -lib/ocaml/coq/ide/xml_lexer.cmi
> -lib/ocaml/coq/ide/xml_parser.cmi
> -lib/ocaml/coq/ide/xml_printer.cmi
> -lib/ocaml/coq/ide/xmlprotocol.cmi
> lib/ocaml/coq/interp/
> +lib/ocaml/coq/interp/constrexpr.cmi
> lib/ocaml/coq/interp/constrexpr_ops.cmi
> lib/ocaml/coq/interp/constrextern.cmi
> lib/ocaml/coq/interp/constrintern.cmi
> @@ -123,25 +131,12 @@ lib/ocaml/coq/interp/implicit_quantifier
> lib/ocaml/coq/interp/modintern.cmi
> lib/ocaml/coq/interp/notation.cmi
> lib/ocaml/coq/interp/notation_ops.cmi
> -lib/ocaml/coq/interp/ppextend.cmi
> +lib/ocaml/coq/interp/notation_term.cmi
> +lib/ocaml/coq/interp/numTok.cmi
> lib/ocaml/coq/interp/reserve.cmi
> lib/ocaml/coq/interp/smartlocate.cmi
> lib/ocaml/coq/interp/stdarg.cmi
> lib/ocaml/coq/interp/syntax_def.cmi
> -lib/ocaml/coq/interp/tactypes.cmi
> -lib/ocaml/coq/interp/topconstr.cmi
> -lib/ocaml/coq/intf/
> -lib/ocaml/coq/intf/constrexpr.cmi
> -lib/ocaml/coq/intf/decl_kinds.cmi
> -lib/ocaml/coq/intf/evar_kinds.cmi
> -lib/ocaml/coq/intf/extend.cmi
> -lib/ocaml/coq/intf/genredexpr.cmi
> -lib/ocaml/coq/intf/glob_term.cmi
> -lib/ocaml/coq/intf/locus.cmi
> -lib/ocaml/coq/intf/misctypes.cmi
> -lib/ocaml/coq/intf/notation_term.cmi
> -lib/ocaml/coq/intf/pattern.cmi
> -lib/ocaml/coq/intf/vernacexpr.cmi
> lib/ocaml/coq/kernel/
> lib/ocaml/coq/kernel/byterun/
> lib/ocaml/coq/kernel/byterun/dllcoqrun.so
> @@ -151,7 +146,6 @@ lib/ocaml/coq/kernel/cPrimitives.cmi
> lib/ocaml/coq/kernel/cbytecodes.cmi
> lib/ocaml/coq/kernel/cbytegen.cmi
> lib/ocaml/coq/kernel/cemitcodes.cmi
> -lib/ocaml/coq/kernel/cinstr.cmi
> lib/ocaml/coq/kernel/clambda.cmi
> lib/ocaml/coq/kernel/constr.cmi
> lib/ocaml/coq/kernel/context.cmi
> @@ -165,6 +159,7 @@ lib/ocaml/coq/kernel/entries.cmi
> lib/ocaml/coq/kernel/environ.cmi
> lib/ocaml/coq/kernel/esubst.cmi
> lib/ocaml/coq/kernel/evar.cmi
> +lib/ocaml/coq/kernel/indTyping.cmi
> lib/ocaml/coq/kernel/indtypes.cmi
> lib/ocaml/coq/kernel/inductive.cmi
> lib/ocaml/coq/kernel/mod_subst.cmi
> @@ -173,30 +168,32 @@ lib/ocaml/coq/kernel/modops.cmi
> lib/ocaml/coq/kernel/names.cmi
> lib/ocaml/coq/kernel/nativecode.cmi
> lib/ocaml/coq/kernel/nativeconv.cmi
> -lib/ocaml/coq/kernel/nativeinstr.cmi
> lib/ocaml/coq/kernel/nativelambda.cmi
> lib/ocaml/coq/kernel/nativelib.cmi
> lib/ocaml/coq/kernel/nativelibrary.cmi
> lib/ocaml/coq/kernel/nativevalues.cmi
> lib/ocaml/coq/kernel/opaqueproof.cmi
> -lib/ocaml/coq/kernel/pre_env.cmi
> +lib/ocaml/coq/kernel/primred.cmi
> lib/ocaml/coq/kernel/reduction.cmi
> lib/ocaml/coq/kernel/retroknowledge.cmi
> +lib/ocaml/coq/kernel/retypeops.cmi
> lib/ocaml/coq/kernel/safe_typing.cmi
> lib/ocaml/coq/kernel/sorts.cmi
> lib/ocaml/coq/kernel/subtyping.cmi
> lib/ocaml/coq/kernel/term.cmi
> lib/ocaml/coq/kernel/term_typing.cmi
> +lib/ocaml/coq/kernel/transparentState.cmi
> lib/ocaml/coq/kernel/type_errors.cmi
> lib/ocaml/coq/kernel/typeops.cmi
> lib/ocaml/coq/kernel/uGraph.cmi
> -lib/ocaml/coq/kernel/uint31.cmi
> +lib/ocaml/coq/kernel/uint63.cmi
> lib/ocaml/coq/kernel/univ.cmi
> lib/ocaml/coq/kernel/vars.cmi
> lib/ocaml/coq/kernel/vconv.cmi
> lib/ocaml/coq/kernel/vm.cmi
> lib/ocaml/coq/kernel/vmvalues.cmi
> lib/ocaml/coq/lib/
> +lib/ocaml/coq/lib/acyclicGraph.cmi
> lib/ocaml/coq/lib/aux_file.cmi
> lib/ocaml/coq/lib/cAst.cmi
> lib/ocaml/coq/lib/cErrors.cmi
> @@ -214,6 +211,7 @@ lib/ocaml/coq/lib/genarg.cmi
> lib/ocaml/coq/lib/hook.cmi
> lib/ocaml/coq/lib/loc.cmi
> lib/ocaml/coq/lib/pp.cmi
> +lib/ocaml/coq/lib/pp_diff.cmi
> lib/ocaml/coq/lib/remoteCounter.cmi
> lib/ocaml/coq/lib/rtree.cmi
> lib/ocaml/coq/lib/spawn.cmi
> @@ -223,13 +221,12 @@ lib/ocaml/coq/lib/util.cmi
> lib/ocaml/coq/lib/xml_datatype.cmi
> lib/ocaml/coq/library/
> lib/ocaml/coq/library/coqlib.cmi
> +lib/ocaml/coq/library/decl_kinds.cmi
> lib/ocaml/coq/library/declaremods.cmi
> lib/ocaml/coq/library/decls.cmi
> -lib/ocaml/coq/library/dischargedhypsmap.cmi
> lib/ocaml/coq/library/global.cmi
> lib/ocaml/coq/library/globnames.cmi
> lib/ocaml/coq/library/goptions.cmi
> -lib/ocaml/coq/library/heads.cmi
> lib/ocaml/coq/library/keys.cmi
> lib/ocaml/coq/library/kindops.cmi
> lib/ocaml/coq/library/lib.cmi
> @@ -242,13 +239,13 @@ lib/ocaml/coq/library/states.cmi
> lib/ocaml/coq/library/summary.cmi
> lib/ocaml/coq/parsing/
> lib/ocaml/coq/parsing/cLexer.cmi
> -lib/ocaml/coq/parsing/egramcoq.cmi
> -lib/ocaml/coq/parsing/egramml.cmi
> +lib/ocaml/coq/parsing/extend.cmi
> lib/ocaml/coq/parsing/g_constr.cmi
> lib/ocaml/coq/parsing/g_prim.cmi
> -lib/ocaml/coq/parsing/g_proofs.cmi
> -lib/ocaml/coq/parsing/g_vernac.cmi
> +lib/ocaml/coq/parsing/notation_gram.cmi
> +lib/ocaml/coq/parsing/notgram_ops.cmi
> lib/ocaml/coq/parsing/pcoq.cmi
> +lib/ocaml/coq/parsing/ppextend.cmi
> lib/ocaml/coq/parsing/tok.cmi
> lib/ocaml/coq/plugins/
> lib/ocaml/coq/plugins/btauto/
> @@ -266,6 +263,7 @@ lib/ocaml/coq/plugins/btauto/Reflect.glo
> lib/ocaml/coq/plugins/btauto/Reflect.v
> lib/ocaml/coq/plugins/btauto/Reflect.vo
> lib/ocaml/coq/plugins/btauto/btauto_plugin.cmi
> +lib/ocaml/coq/plugins/btauto/refl_btauto.cmi
> lib/ocaml/coq/plugins/cc/
> lib/ocaml/coq/plugins/cc/cc_plugin.cmi
> lib/ocaml/coq/plugins/cc/ccalgo.cmi
> @@ -369,17 +367,6 @@ lib/ocaml/coq/plugins/firstorder/instanc
> lib/ocaml/coq/plugins/firstorder/rules.cmi
> lib/ocaml/coq/plugins/firstorder/sequent.cmi
> lib/ocaml/coq/plugins/firstorder/unify.cmi
> -lib/ocaml/coq/plugins/fourier/
> -lib/ocaml/coq/plugins/fourier/.coq-native/
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmi
> -lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmi
> -lib/ocaml/coq/plugins/fourier/Fourier.glob
> -lib/ocaml/coq/plugins/fourier/Fourier.v
> -lib/ocaml/coq/plugins/fourier/Fourier.vo
> -lib/ocaml/coq/plugins/fourier/Fourier_util.glob
> -lib/ocaml/coq/plugins/fourier/Fourier_util.v
> -lib/ocaml/coq/plugins/fourier/Fourier_util.vo
> -lib/ocaml/coq/plugins/fourier/fourier_plugin.cmi
> lib/ocaml/coq/plugins/funind/
> lib/ocaml/coq/plugins/funind/.coq-native/
> lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmi
> @@ -428,8 +415,11 @@ lib/ocaml/coq/plugins/ltac/tauto.cmi
> lib/ocaml/coq/plugins/ltac/tauto_plugin.cmi
> lib/ocaml/coq/plugins/micromega/
> lib/ocaml/coq/plugins/micromega/.coq-native/
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmi
> +lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
> @@ -444,12 +434,21 @@ lib/ocaml/coq/plugins/micromega/.coq-nat
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmi
> lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmi
> +lib/ocaml/coq/plugins/micromega/DeclConstant.glob
> +lib/ocaml/coq/plugins/micromega/DeclConstant.v
> +lib/ocaml/coq/plugins/micromega/DeclConstant.vo
> lib/ocaml/coq/plugins/micromega/Env.glob
> lib/ocaml/coq/plugins/micromega/Env.v
> lib/ocaml/coq/plugins/micromega/Env.vo
> lib/ocaml/coq/plugins/micromega/EnvRing.glob
> lib/ocaml/coq/plugins/micromega/EnvRing.v
> lib/ocaml/coq/plugins/micromega/EnvRing.vo
> +lib/ocaml/coq/plugins/micromega/Fourier.glob
> +lib/ocaml/coq/plugins/micromega/Fourier.v
> +lib/ocaml/coq/plugins/micromega/Fourier.vo
> +lib/ocaml/coq/plugins/micromega/Fourier_util.glob
> +lib/ocaml/coq/plugins/micromega/Fourier_util.v
> +lib/ocaml/coq/plugins/micromega/Fourier_util.vo
> lib/ocaml/coq/plugins/micromega/Lia.glob
> lib/ocaml/coq/plugins/micromega/Lia.v
> lib/ocaml/coq/plugins/micromega/Lia.vo
> @@ -492,11 +491,23 @@ lib/ocaml/coq/plugins/micromega/ZCoeff.v
> lib/ocaml/coq/plugins/micromega/ZMicromega.glob
> lib/ocaml/coq/plugins/micromega/ZMicromega.v
> lib/ocaml/coq/plugins/micromega/ZMicromega.vo
> +lib/ocaml/coq/plugins/micromega/certificate.cmi
> +lib/ocaml/coq/plugins/micromega/coq_micromega.cmi
> @bin lib/ocaml/coq/plugins/micromega/csdpcert
> +lib/ocaml/coq/plugins/micromega/csdpcert.cmi
> +lib/ocaml/coq/plugins/micromega/g_micromega.cmi
> +lib/ocaml/coq/plugins/micromega/itv.cmi
> +lib/ocaml/coq/plugins/micromega/mfourier.cmi
> lib/ocaml/coq/plugins/micromega/micromega.cmi
> lib/ocaml/coq/plugins/micromega/micromega_plugin.cmi
> +lib/ocaml/coq/plugins/micromega/mutils.cmi
> +lib/ocaml/coq/plugins/micromega/persistent_cache.cmi
> +lib/ocaml/coq/plugins/micromega/polynomial.cmi
> +lib/ocaml/coq/plugins/micromega/simplex.cmi
> lib/ocaml/coq/plugins/micromega/sos.cmi
> +lib/ocaml/coq/plugins/micromega/sos_lib.cmi
> lib/ocaml/coq/plugins/micromega/sos_types.cmi
> +lib/ocaml/coq/plugins/micromega/vect.cmi
> lib/ocaml/coq/plugins/nsatz/
> lib/ocaml/coq/plugins/nsatz/.coq-native/
> lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
> @@ -530,26 +541,8 @@ lib/ocaml/coq/plugins/omega/OmegaTactic.
> lib/ocaml/coq/plugins/omega/PreOmega.glob
> lib/ocaml/coq/plugins/omega/PreOmega.v
> lib/ocaml/coq/plugins/omega/PreOmega.vo
> +lib/ocaml/coq/plugins/omega/coq_omega.cmi
> lib/ocaml/coq/plugins/omega/omega_plugin.cmi
> -lib/ocaml/coq/plugins/quote/
> -lib/ocaml/coq/plugins/quote/.coq-native/
> -lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
> -lib/ocaml/coq/plugins/quote/Quote.glob
> -lib/ocaml/coq/plugins/quote/Quote.v
> -lib/ocaml/coq/plugins/quote/Quote.vo
> -lib/ocaml/coq/plugins/quote/quote_plugin.cmi
> -lib/ocaml/coq/plugins/romega/
> -lib/ocaml/coq/plugins/romega/.coq-native/
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
> -lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi
> -lib/ocaml/coq/plugins/romega/ROmega.glob
> -lib/ocaml/coq/plugins/romega/ROmega.v
> -lib/ocaml/coq/plugins/romega/ROmega.vo
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.glob
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.v
> -lib/ocaml/coq/plugins/romega/ReflOmegaCore.vo
> -lib/ocaml/coq/plugins/romega/const_omega.cmi
> -lib/ocaml/coq/plugins/romega/romega_plugin.cmi
> lib/ocaml/coq/plugins/rtauto/
> lib/ocaml/coq/plugins/rtauto/.coq-native/
> lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
> @@ -694,18 +687,20 @@ lib/ocaml/coq/plugins/ssr/ssrview.cmi
> lib/ocaml/coq/plugins/ssrmatching/
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/
> lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
> +lib/ocaml/coq/plugins/ssrmatching/g_ssrmatching.cmi
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.cmi
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.glob
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.v
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching.vo
> lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
> lib/ocaml/coq/plugins/syntax/
> -lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/numeral.cmi
> +lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/r_syntax.cmi
> lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmi
> -lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmi
> +lib/ocaml/coq/plugins/syntax/string_notation.cmi
> +lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmi
> lib/ocaml/coq/pretyping/
> lib/ocaml/coq/pretyping/arguments_renaming.cmi
> lib/ocaml/coq/pretyping/cases.cmi
> @@ -719,20 +714,23 @@ lib/ocaml/coq/pretyping/evardefine.cmi
> lib/ocaml/coq/pretyping/evarsolve.cmi
> lib/ocaml/coq/pretyping/find_subterm.cmi
> lib/ocaml/coq/pretyping/geninterp.cmi
> +lib/ocaml/coq/pretyping/globEnv.cmi
> lib/ocaml/coq/pretyping/glob_ops.cmi
> +lib/ocaml/coq/pretyping/glob_term.cmi
> +lib/ocaml/coq/pretyping/heads.cmi
> lib/ocaml/coq/pretyping/indrec.cmi
> lib/ocaml/coq/pretyping/inductiveops.cmi
> lib/ocaml/coq/pretyping/inferCumulativity.cmi
> +lib/ocaml/coq/pretyping/locus.cmi
> lib/ocaml/coq/pretyping/locusops.cmi
> lib/ocaml/coq/pretyping/ltac_pretype.cmi
> -lib/ocaml/coq/pretyping/miscops.cmi
> lib/ocaml/coq/pretyping/nativenorm.cmi
> +lib/ocaml/coq/pretyping/pattern.cmi
> lib/ocaml/coq/pretyping/patternops.cmi
> lib/ocaml/coq/pretyping/pretype_errors.cmi
> lib/ocaml/coq/pretyping/pretyping.cmi
> lib/ocaml/coq/pretyping/program.cmi
> lib/ocaml/coq/pretyping/recordops.cmi
> -lib/ocaml/coq/pretyping/redops.cmi
> lib/ocaml/coq/pretyping/reductionops.cmi
> lib/ocaml/coq/pretyping/retyping.cmi
> lib/ocaml/coq/pretyping/tacred.cmi
> @@ -740,32 +738,32 @@ lib/ocaml/coq/pretyping/typeclasses.cmi
> lib/ocaml/coq/pretyping/typeclasses_errors.cmi
> lib/ocaml/coq/pretyping/typing.cmi
> lib/ocaml/coq/pretyping/unification.cmi
> -lib/ocaml/coq/pretyping/univdecls.cmi
> lib/ocaml/coq/pretyping/vnorm.cmi
> lib/ocaml/coq/printing/
> lib/ocaml/coq/printing/genprint.cmi
> lib/ocaml/coq/printing/ppconstr.cmi
> lib/ocaml/coq/printing/pputils.cmi
> -lib/ocaml/coq/printing/ppvernac.cmi
> lib/ocaml/coq/printing/prettyp.cmi
> lib/ocaml/coq/printing/printer.cmi
> lib/ocaml/coq/printing/printmod.cmi
> +lib/ocaml/coq/printing/proof_diffs.cmi
> lib/ocaml/coq/proofs/
> lib/ocaml/coq/proofs/clenv.cmi
> lib/ocaml/coq/proofs/clenvtac.cmi
> lib/ocaml/coq/proofs/evar_refiner.cmi
> lib/ocaml/coq/proofs/goal.cmi
> +lib/ocaml/coq/proofs/goal_select.cmi
> lib/ocaml/coq/proofs/logic.cmi
> lib/ocaml/coq/proofs/miscprint.cmi
> lib/ocaml/coq/proofs/pfedit.cmi
> lib/ocaml/coq/proofs/proof.cmi
> lib/ocaml/coq/proofs/proof_bullet.cmi
> lib/ocaml/coq/proofs/proof_global.cmi
> -lib/ocaml/coq/proofs/proof_type.cmi
> -lib/ocaml/coq/proofs/redexpr.cmi
> lib/ocaml/coq/proofs/refine.cmi
> lib/ocaml/coq/proofs/refiner.cmi
> lib/ocaml/coq/proofs/tacmach.cmi
> +lib/ocaml/coq/proofs/tactypes.cmi
> +lib/ocaml/coq/revision
> lib/ocaml/coq/stm/
> lib/ocaml/coq/stm/asyncTaskQueue.cmi
> lib/ocaml/coq/stm/coqworkmgrApi.cmi
> @@ -777,9 +775,9 @@ lib/ocaml/coq/stm/tQueue.cmi
> lib/ocaml/coq/stm/vcs.cmi
> lib/ocaml/coq/stm/vernac_classifier.cmi
> lib/ocaml/coq/stm/vio_checking.cmi
> -lib/ocaml/coq/stm/workerLoop.cmi
> lib/ocaml/coq/stm/workerPool.cmi
> lib/ocaml/coq/tactics/
> +lib/ocaml/coq/tactics/abstract.cmi
> lib/ocaml/coq/tactics/auto.cmi
> lib/ocaml/coq/tactics/autorewrite.cmi
> lib/ocaml/coq/tactics/btermdn.cmi
> @@ -793,11 +791,15 @@ lib/ocaml/coq/tactics/elimschemes.cmi
> lib/ocaml/coq/tactics/eqdecide.cmi
> lib/ocaml/coq/tactics/eqschemes.cmi
> lib/ocaml/coq/tactics/equality.cmi
> +lib/ocaml/coq/tactics/genredexpr.cmi
> lib/ocaml/coq/tactics/hints.cmi
> lib/ocaml/coq/tactics/hipattern.cmi
> lib/ocaml/coq/tactics/ind_tables.cmi
> lib/ocaml/coq/tactics/inv.cmi
> lib/ocaml/coq/tactics/leminv.cmi
> +lib/ocaml/coq/tactics/ppred.cmi
> +lib/ocaml/coq/tactics/redexpr.cmi
> +lib/ocaml/coq/tactics/redops.cmi
> lib/ocaml/coq/tactics/tacticals.cmi
> lib/ocaml/coq/tactics/tactics.cmi
> lib/ocaml/coq/tactics/term_dnet.cmi
> @@ -987,21 +989,21 @@ lib/ocaml/coq/theories/Classes/SetoidTac
> lib/ocaml/coq/theories/Compat/
> lib/ocaml/coq/theories/Compat/.coq-native/
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi
> -lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmi
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmi
> lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmi
> +lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmi
> lib/ocaml/coq/theories/Compat/AdmitAxiom.glob
> lib/ocaml/coq/theories/Compat/AdmitAxiom.v
> lib/ocaml/coq/theories/Compat/AdmitAxiom.vo
> -lib/ocaml/coq/theories/Compat/Coq86.glob
> -lib/ocaml/coq/theories/Compat/Coq86.v
> -lib/ocaml/coq/theories/Compat/Coq86.vo
> -lib/ocaml/coq/theories/Compat/Coq87.glob
> -lib/ocaml/coq/theories/Compat/Coq87.v
> -lib/ocaml/coq/theories/Compat/Coq87.vo
> +lib/ocaml/coq/theories/Compat/Coq810.glob
> +lib/ocaml/coq/theories/Compat/Coq810.v
> +lib/ocaml/coq/theories/Compat/Coq810.vo
> lib/ocaml/coq/theories/Compat/Coq88.glob
> lib/ocaml/coq/theories/Compat/Coq88.v
> lib/ocaml/coq/theories/Compat/Coq88.vo
> +lib/ocaml/coq/theories/Compat/Coq89.glob
> +lib/ocaml/coq/theories/Compat/Coq89.v
> +lib/ocaml/coq/theories/Compat/Coq89.vo
> lib/ocaml/coq/theories/FSets/
> lib/ocaml/coq/theories/FSets/.coq-native/
> lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
> @@ -1090,6 +1092,7 @@ lib/ocaml/coq/theories/FSets/FSets.v
> lib/ocaml/coq/theories/FSets/FSets.vo
> lib/ocaml/coq/theories/Init/
> lib/ocaml/coq/theories/Init/.coq-native/
> +lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmi
> @@ -1102,6 +1105,9 @@ lib/ocaml/coq/theories/Init/.coq-native/
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi
> lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi
> +lib/ocaml/coq/theories/Init/Byte.glob
> +lib/ocaml/coq/theories/Init/Byte.v
> +lib/ocaml/coq/theories/Init/Byte.vo
> lib/ocaml/coq/theories/Init/Datatypes.glob
> lib/ocaml/coq/theories/Init/Datatypes.v
> lib/ocaml/coq/theories/Init/Datatypes.vo
> @@ -1207,6 +1213,7 @@ lib/ocaml/coq/theories/Logic/.coq-native
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmi
> +lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmi
> lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmi
> lib/ocaml/coq/theories/Logic/Berardi.glob
> @@ -1308,6 +1315,9 @@ lib/ocaml/coq/theories/Logic/SetIsType.v
> lib/ocaml/coq/theories/Logic/SetoidChoice.glob
> lib/ocaml/coq/theories/Logic/SetoidChoice.v
> lib/ocaml/coq/theories/Logic/SetoidChoice.vo
> +lib/ocaml/coq/theories/Logic/StrictProp.glob
> +lib/ocaml/coq/theories/Logic/StrictProp.v
> +lib/ocaml/coq/theories/Logic/StrictProp.vo
> lib/ocaml/coq/theories/Logic/WKL.glob
> lib/ocaml/coq/theories/Logic/WKL.v
> lib/ocaml/coq/theories/Logic/WKL.vo
> @@ -1412,6 +1422,7 @@ lib/ocaml/coq/theories/NArith/Nsqrt_def.
> lib/ocaml/coq/theories/NArith/Nsqrt_def.vo
> lib/ocaml/coq/theories/Numbers/
> lib/ocaml/coq/theories/Numbers/.coq-native/
> +lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmi
> @@ -1421,6 +1432,9 @@ lib/ocaml/coq/theories/Numbers/.coq-nati
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmi
> lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmi
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.glob
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.v
> +lib/ocaml/coq/theories/Numbers/AltBinNotations.vo
> lib/ocaml/coq/theories/Numbers/BinNums.glob
> lib/ocaml/coq/theories/Numbers/BinNums.v
> lib/ocaml/coq/theories/Numbers/BinNums.vo
> @@ -1453,6 +1467,20 @@ lib/ocaml/coq/theories/Numbers/Cyclic/In
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.glob
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.v
> lib/ocaml/coq/theories/Numbers/Cyclic/Int31/Ring31.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmi
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Cyclic63.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Int63.vo
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.glob
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.v
> +lib/ocaml/coq/theories/Numbers/Cyclic/Int63/Ring63.vo
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/
> lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmi
> @@ -1904,6 +1932,7 @@ lib/ocaml/coq/theories/Reals/.coq-native
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmi
> +lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmi
> lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmi
> @@ -2080,6 +2109,9 @@ lib/ocaml/coq/theories/Reals/Rtrigo_fun.
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.glob
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.v
> lib/ocaml/coq/theories/Reals/Rtrigo_reg.vo
> +lib/ocaml/coq/theories/Reals/Runcountable.glob
> +lib/ocaml/coq/theories/Reals/Runcountable.v
> +lib/ocaml/coq/theories/Reals/Runcountable.vo
> lib/ocaml/coq/theories/Reals/SeqProp.glob
> lib/ocaml/coq/theories/Reals/SeqProp.v
> lib/ocaml/coq/theories/Reals/SeqProp.vo
> @@ -2242,10 +2274,30 @@ lib/ocaml/coq/theories/Sorting/Sorting.v
> lib/ocaml/coq/theories/Strings/
> lib/ocaml/coq/theories/Strings/.coq-native/
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmi
> +lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmi
> lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmi
> lib/ocaml/coq/theories/Strings/Ascii.glob
> lib/ocaml/coq/theories/Strings/Ascii.v
> lib/ocaml/coq/theories/Strings/Ascii.vo
> +lib/ocaml/coq/theories/Strings/BinaryString.glob
> +lib/ocaml/coq/theories/Strings/BinaryString.v
> +lib/ocaml/coq/theories/Strings/BinaryString.vo
> +lib/ocaml/coq/theories/Strings/Byte.glob
> +lib/ocaml/coq/theories/Strings/Byte.v
> +lib/ocaml/coq/theories/Strings/Byte.vo
> +lib/ocaml/coq/theories/Strings/ByteVector.glob
> +lib/ocaml/coq/theories/Strings/ByteVector.v
> +lib/ocaml/coq/theories/Strings/ByteVector.vo
> +lib/ocaml/coq/theories/Strings/HexString.glob
> +lib/ocaml/coq/theories/Strings/HexString.v
> +lib/ocaml/coq/theories/Strings/HexString.vo
> +lib/ocaml/coq/theories/Strings/OctalString.glob
> +lib/ocaml/coq/theories/Strings/OctalString.v
> +lib/ocaml/coq/theories/Strings/OctalString.vo
> lib/ocaml/coq/theories/Strings/String.glob
> lib/ocaml/coq/theories/Strings/String.v
> lib/ocaml/coq/theories/Strings/String.vo
> @@ -2520,17 +2572,23 @@ lib/ocaml/coq/tools/coqdoc/coqdoc.sty
> lib/ocaml/coq/tools/make-both-single-timing-files.py
> lib/ocaml/coq/tools/make-both-time-files.py
> lib/ocaml/coq/tools/make-one-time-file.py
> +lib/ocaml/coq/topbin/
> lib/ocaml/coq/toplevel/
> +lib/ocaml/coq/toplevel/ccompile.cmi
> lib/ocaml/coq/toplevel/coqargs.cmi
> +lib/ocaml/coq/toplevel/coqc.cmi
> +lib/ocaml/coq/toplevel/coqcargs.cmi
> lib/ocaml/coq/toplevel/coqinit.cmi
> lib/ocaml/coq/toplevel/coqloop.cmi
> lib/ocaml/coq/toplevel/coqtop.cmi
> +lib/ocaml/coq/toplevel/g_toplevel.cmi
> lib/ocaml/coq/toplevel/usage.cmi
> lib/ocaml/coq/toplevel/vernac.cmi
> -lib/ocaml/coq/toploop/
> +lib/ocaml/coq/toplevel/workerLoop.cmi
> lib/ocaml/coq/user-contrib/
> lib/ocaml/coq/vernac/
> lib/ocaml/coq/vernac/assumptions.cmi
> +lib/ocaml/coq/vernac/attributes.cmi
> lib/ocaml/coq/vernac/auto_ind_decl.cmi
> lib/ocaml/coq/vernac/class.cmi
> lib/ocaml/coq/vernac/classes.cmi
> @@ -2540,7 +2598,11 @@ lib/ocaml/coq/vernac/comFixpoint.cmi
> lib/ocaml/coq/vernac/comInductive.cmi
> lib/ocaml/coq/vernac/comProgramFixpoint.cmi
> lib/ocaml/coq/vernac/declareDef.cmi
> +lib/ocaml/coq/vernac/egramcoq.cmi
> +lib/ocaml/coq/vernac/egramml.cmi
> lib/ocaml/coq/vernac/explainErr.cmi
> +lib/ocaml/coq/vernac/g_proofs.cmi
> +lib/ocaml/coq/vernac/g_vernac.cmi
> lib/ocaml/coq/vernac/himsg.cmi
> lib/ocaml/coq/vernac/indschemes.cmi
> lib/ocaml/coq/vernac/lemmas.cmi
> @@ -2548,12 +2610,15 @@ lib/ocaml/coq/vernac/locality.cmi
> lib/ocaml/coq/vernac/metasyntax.cmi
> lib/ocaml/coq/vernac/mltop.cmi
> lib/ocaml/coq/vernac/obligations.cmi
> +lib/ocaml/coq/vernac/ppvernac.cmi
> lib/ocaml/coq/vernac/proof_using.cmi
> +lib/ocaml/coq/vernac/pvernac.cmi
> lib/ocaml/coq/vernac/record.cmi
> lib/ocaml/coq/vernac/search.cmi
> lib/ocaml/coq/vernac/topfmt.cmi
> lib/ocaml/coq/vernac/vernacentries.cmi
> -lib/ocaml/coq/vernac/vernacinterp.cmi
> +lib/ocaml/coq/vernac/vernacexpr.cmi
> +lib/ocaml/coq/vernac/vernacextend.cmi
> lib/ocaml/coq/vernac/vernacprop.cmi
> lib/ocaml/coq/vernac/vernacstate.cmi
> @man man/man1/coq-tex.1
> @@ -2567,26 +2632,18 @@ lib/ocaml/coq/vernac/vernacstate.cmi
> @man man/man1/coqtop.byte.1
> @man man/man1/coqtop.opt.1
> @man man/man1/coqwc.1
> -@man man/man1/gallina.1
> share/coq/
> share/coq/coq-ssreflect.lang
> share/coq/coq.lang
> share/coq/coq.png
> share/coq/coq_style.xml
> +share/coq/default.bindings
> share/doc/coq/
> -share/doc/coq/CHANGES
> share/doc/coq/CONTRIBUTING.md
> share/doc/coq/CREDITS
> share/doc/coq/FAQ-CoqIde
> share/doc/coq/LICENSE
> share/doc/coq/README.md
> -share/emacs/
> -share/emacs/site-lisp/
> -share/emacs/site-lisp/coq-font-lock.el
> -share/emacs/site-lisp/gallina-db.el
> -share/emacs/site-lisp/gallina-syntax.el
> -share/emacs/site-lisp/gallina.el
> -share/emacs/site-lisp/inferior-coq.el
> share/texmf/
> share/texmf/tex/
> share/texmf/tex/latex/
>
>
> --
> http://gmerlin.de
> OpenPGP: http://gmerlin.de/christopher.pub
> CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1