如何在法新社跳过有问题的伊莎贝尔会议？

如何解决如何在法新社跳过有问题的伊莎贝尔会议？

我尝试将 AFP (02/22/2021) 与 Isabelle 2021 一起使用，但是在将 AFP 目录添加到用户 ROOT 文件后，jEdit/Isabelle PIDE 无法加载。如下所示，似乎与特定包有关：

我真的不需要有问题的条目（或知道它的作用）。我的问题是：

有没有办法使用 AFP 的子集并在屏幕截图中排除有问题的条目？

-- 更新 ---

正如评论中所指出的，法新社似乎落后了几天。使用 afp-02-24-2021，初始错误消失了。但是，当从 jEdit 中选择会话 Jordan-normal-Form 时，出现了一个关于 JNF-AFP-Lib 构建失败的新错误，如下所示：

问题依旧。 AFP 似乎是一个大集合，可能有多种错误来源。

如果出现此类错误，有没有办法选择 AFP 的子集来使用或调试？

如果没有，是否有系统的方法来测试哪些 afps 构建或不构建？

解决方法

原始问题

问题是因为您（在不知不觉中）使用了与 Isabelle 版本不匹配的 AFP 版本。为避免将来出现该问题，我建议直接使用 Mercurial 存储库：

https://foss.heptapod.net/isa-afp/afp-2021

新 Isabelle 版本的 Mercurial 存储库是在 RC 阶段创建的，因此您始终可以确保拥有匹配的版本。

在这些不匹配的情况下，通常无法选择“有效”的 AFP 子集，因为在 2020 年到 2021 年之间，会话管理发生了很大变化。

更新

您在这里面临的问题是您选择了大型会话作为先决条件，并且使用默认配置构建需要很长时间。

您可以在命令行上构建会话并增加超时时间，如下所示：

<template>
  <div id="app" v-bind:class="{ darkMode: isDark }" v-cloak>
    <div class="upperBar">
      <a href="/"><img src="./assets/NewIconBlack.png" id="logo"></a>
      <Logo msg="MEETINK"/>
      <Nav />
    </div>
    <router-view />
    <div class="login_register">
      <Login />
      <Register />
    </div>
  </div>
</template>

<script>
import Logo from './components/Logo.vue'
import Login from './components/Login.vue'
import Register from './components/Register.vue'
import Nav from './components/Nav.vue'
import firebase from 'firebase'  
require('firebase/auth')
import db from './main'

export default {
  name: 'App',components: {
    Logo,Login,Register,Nav
  },data() {
    return {
      isDark: false
    }
  },mounted() {
       firebase.auth().onAuthStateChanged(user => {
                if(user){
                     const modeRef = db.collection('modes');
                    /*modeRef.doc(firebase.auth().currentUser.uid).get().then(doc => {
                            if(doc.data().backgroundMode === 'dark'){
                              this.isDark = true
                            }else {
                              this.isDark = false
                            }
                    })*/
                    modeRef.doc(firebase.auth().currentUser.uid).onSnapshot(querySnapshot => {
                            if(querySnapshot.data().backgroundMode === 'dark'){
                              this.isDark = true
                            }else {
                              this.isDark = false
                            }
                    })
                }else {
                    this.$router.push('/')
                }
            })
  }
}
</script>

<style>
* {
  margin: 0;
  padding: 0;
  box-sizing: border-box;
}

.login_register{
  float: right;
  width: 20%;
}

html,body {
  height: 100%;
  width: 100%;
}

#app {
  font-family: Avenir,Helvetica,Arial,sans-serif;
  -webkit-font-smoothing: antialiased;
  -moz-osx-font-smoothing: grayscale;
  text-align: center;
  color: #2c3e50;
  margin-top: 0;
  height: 100%;
  width: 100%;
}

[v-cloak] { 
  display: none!important; 
}

#logo {
  height: 50px;
  width: auto;
  float: left;
  margin: 15px;
}

.upperBar {
  width: 100%;
  height: 80px;
  -webkit-box-shadow: 0px 7px 20px 6px rgba(0,0.2); 
  box-shadow: 0px 7px 20px 6px rgba(0,0.2);
}

.darkMode {
  background-color: rgb(30,30,30);
  -webkit-box-shadow: 0px 7px 20px 6px rgba(0,0.2);
  color: rgb(105,126,147)!important;
}
</style>

如果它一直超时，则增加因子。

一般备注

您会问：“如果出现此类错误，是否可以选择 AFP 的子集进行使用或调试？”。这个问题的答案取决于错误的类型。您的帖子目前包含两个截然不同的问题，因此很遗憾，无法给出一般性答案。