The predata stage now automatically includes the .tlean and .ast.json files for archive and counterexamples in the mathlib3-predata.tar.gz export.
There are two new synport exports, archive-synport.tar.gz and counterexamples-synport.tar.gz, containing the mathported syntax files. The binport data is not being exported.
The update.sh script on mathlib3port needs to be updated if we want it to unpack these files into the repo.
predatastage now automatically includes the.tleanand.ast.jsonfiles forarchiveandcounterexamplesin themathlib3-predata.tar.gzexport.archive-synport.tar.gzandcounterexamples-synport.tar.gz, containing the mathported syntax files. The binport data is not being exported.update.shscript onmathlib3portneeds to be updated if we want it to unpack these files into the repo.