首页
学习
活动
专区
工具
TVP
发布
精选内容/技术社群/优惠产品,尽在小程序
立即前往

在打开emacs时添加路径到coqtop时,“Symbol的值作为变量是空的”

在打开emacs时添加路径到coqtop时,"Symbol的值作为变量是空的"是指在配置coqtop路径时,emacs无法找到该路径所对应的符号变量。

要解决这个问题,可以按照以下步骤进行操作:

  1. 确保coqtop已经正确安装并且可执行。可以通过在终端中输入coqtop命令来检查。
  2. 打开emacs,并找到配置文件。通常,emacs的配置文件是.emacs或者.emacs.d/init.el
  3. 在配置文件中找到coq的配置部分。这通常是以(require 'coq)或者(load "coq.el")开头的一段代码。
  4. 在coq的配置部分中,找到设置coqtop路径的代码。这通常是以(setq coq-prog-name "coqtop")或者(setq coq-prog-name "/path/to/coqtop")的形式存在。
  5. 确保coqtop的路径设置正确。如果你已经知道coqtop的路径,直接将路径替换到上述代码中的/path/to/coqtop部分。如果不知道coqtop的路径,可以在终端中输入which coqtop命令来查找。
  6. 保存配置文件,并重新启动emacs。

如果仍然出现"Symbol的值作为变量是空的"的错误提示,可能是由于配置文件中的其他问题导致的。可以尝试检查其他相关的配置项,或者查看emacs的错误日志以获取更多信息。

关于coq和emacs的更多信息,可以参考以下链接:

  • Coq官方网站:https://coq.inria.fr/
  • Emacs官方网站:https://www.gnu.org/software/emacs/

请注意,以上提供的链接和产品介绍是基于腾讯云的相关产品和服务,仅供参考。

相关搜索:Emacs: Symbol的值作为变量是空的: Removes (init.el)检查表在计算空值时是相等的。如何使cargo在添加debuginfo到exectuable时,输入到stdlib源文件的正确路径在kubernetes中使用`status.hostIP`作为我的环境变量的引用字段时,变量为空当null作为参数传递时,是否是使用不可为空参数的默认值的方法?为什么我的web API在发布到web api时收到空值?当通过javascript添加"目标":"空白"到链接时,打开的标签是"回收"(重复使用) - 任何防止方法?Rails : simple_form中的下拉列表在定向到编辑路径时不保留值如何自动增加输入字段(type=text)中的值,该值是在单击按钮时动态添加的?在mysql表中创建要导入的csv时,是否需要为索引添加空值?当你在Angular中延迟加载了路径为空的模块时,如何重定向到仪表板?当我的软件包是嵌套依赖项时,一些文件不会安装,即使它们在作为直接依赖项添加时安装在不丢失旧函数的情况下,在每次运行新函数时向变量添加新值(jQuery)在创建列表时,"Amounts_list“看起来没有将值添加到列表中。我得到的值是None在将数据添加到将列表作为其值保存的字典中时,我之前的所有键都将使用列表的最新值进行更新在React Native中导航到另一个类时,有没有办法将变量作为我的类名进行传递?为什么在将excel文件导入到有布尔值列的GridView时,GridView会在相关列中自动添加CheckBoxes当我尝试将csv数据框中的列添加到在pandas上打开的现有数据框中时,为什么我一直得到'Nan‘值?如果索引范围没有获得替换值的完整列表,为什么在将字符串作为列表替换添加时,字符串会被拆分成字母?C++:当您的输入是字符串值时,尝试在二进制到十进制转换器中多次将非常大的整数相加
相关搜索:
页面内容是否对你有帮助?
有帮助
没帮助

相关·内容

  • vim 插件管理与推荐

    编辑器对于所有人来说都再熟悉不过,不论是任何学历、任何工作的人,只要接触电脑,总要录入一些文字,这个时候必将有一款编辑器进入你的视野。 事实上,无论是 vim、emacs 还是如今风靡的各种甜品级编辑器,他们最为吸引人的无不在于他们那超级强大的定制化能力,这也是几十年来,vim 与 emacs 仍然能够走在前列的原因,他们的背后都有着强大的社区,不断为他们产出着一个又一个优秀的扩展,让他们不断焕发耀眼的光芒,而 vim8 与 neovim 的诞生,更让人领略到这宝刀不老的风采。 作为一个 vim 铁杆拥趸,本文就来聊一聊博主心中 vim 最强大的几个插件以及安装、使用方法。

    01

    emacs配置文件3

    ;;普通设置 (setq inhibit-startup-message t);关闭起动时闪屏 (setq visible-bell t);关闭出错时的提示声 (show-paren-mode t);显示括号匹配 ;(set-default-font "-adobe-courier-medium-r-normal--14-100-100-100-m-90-iso10646-1");;字体设置 (column-number-mode t);显示列号 (setq frame-title-format "%n%F/%b");在窗口的标题栏上显示文件名称 (mouse-avoidance-mode 'animate);光标靠近鼠标指针时,让鼠标指针自动让开 (setq default-frame-alist '((height . 25) (width . 80) (menu-bar-lines . 80) (tool-bar-lines . 80)));设置窗口启动大小 (fset 'yes-or-no-p 'y-or-n-p);以 y/n代表 yes/no (setq-default make-backup-files nil);;不要生成临时文件 (setq x-select-enable-clipboard t);;允许emacs和外部其他程序的粘贴 (setq mouse-yank-at-point t);支持中键粘贴 ;(show-paren-mode 't); 高亮显示匹配括号 ;;自动插入匹配的括号 ;; enable skeleton-pair insert globally (setq skeleton-pair t) (global-set-key (kbd "(") 'skeleton-pair-insert-maybe) (global-set-key (kbd "[") 'skeleton-pair-insert-maybe) (global-set-key (kbd "{") 'skeleton-pair-insert-maybe) ;;热键设置 (global-set-key [f9] 'delete-window);F9 关闭d当前窗口 (global-set-key [f8] 'other-window);F8窗口间跳转 (global-set-key [(f2)] 'ansi-term);F2 切换到shell模式 ;(global-set-key [f3] 'split-window-vertically);F3分割窗口 (global-set-key [f12] 'my-fullscreen);F12 全屏 (global-set-key [(f4)] 'compile);编译 (global-set-key [f5] 'gdb);启动gdb (global-set-key [(f6)] 'gdb-many-windows);启动窗口gdb (global-set-key [f1] 'goto-line);设置M-g为goto-line ;(global-set-key [f7] 'other-frame);跳到其它窗格 (global-set-key [(f3)] 'speedbar);打开speedbar ;;显示行号 (load-file "~/dos/emacs/display-line-number.el") ;;(autoload `display-line-number-mode-on "display-line-number" "display mode" t) (require 'display-line-number) (global-display-line-number-mode t) ;;鼠标滚轮,默认的滚动太快,这里改为3行 (defun up-slightly () (interactive) (scroll-up 3)) (defun down-slightly () (interactive) (scroll-down 3)) (global-set-key [mouse-4] 'down-slightly) (global-set-key [mouse-5] 'up-slightly) ;;代码折 (add-hook 'c-mode-hook 'hs-minor-mode) (add-hook 'c++-mode-hook 'hs-minor-mode)   ;全屏 (defun my-fullscreen ()   (interactive)   (x-send-client-message    nil 0 nil "_NET_WM_STATE" 32    '(

    03
    领券