Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Sum_of_Powers and "potential disaster"


view this post on Zulip Email Gateway (Aug 26 2022 at 11:46):

From: Lawrence Paulson <lp15@cam.ac.uk>
I finally deleted HOL-ex.Sum_of_Powers. The testboard job eventually failed with the following message, which I’ve seen a lot lately, so I assume it’s irrelevant to my change.

Larry

Presentation in "/media/data/jenkins/workspace/testboard/browser_info"
01:40:34 *** Existing content in "/media/data/jenkins/workspace/testboard/browser_info" lacks ".browser_info" meta data.
01:40:34 *** To avoid potential disaster, it has not been changed automatically.
01:40:34 *** If this is the intended directory, please move/remove/empty it manually.
01:40:35 Build step 'Execute shell' marked build as failure


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Aug 26 2022 at 14:13):

From: Makarius <makarius@sketis.net>
I wrote this exceedingly explicit error message to avoid additional
documentation and explanations.

Someone with access to the Jenkins setup needs to do what the messages says.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC