search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

sertop can't be found #69

Closed arthurpaulino closed 2 years ago

arthurpaulino commented 2 years ago

I've already installed coq-serapi with opam, but when I try to run alectryon it says that sertop needs to be installed. But if I try to run the proposed command, it says that coq-serapi is already installed:

(exp) arthur@metamind:~$ alectryon lf/Basics.v
Exiting early due to an error; use --traceback to diagnose:
  `sertop` binary not found (bin=sertop); please run `opam install coq-serapi`
(exp) arthur@metamind:~$ opam install coq-serapi
[NOTE] Package coq-serapi is already installed (current version is 8.13.0+0.13.0).
arthurpaulino commented 2 years ago

This is the output of pip show alectryon:

(exp) arthur@metamind:~$ pip show alectryon
Name: alectryon
Version: 1.4.0
Summary: A library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence.
Home-page: https://github.com/cpitclaudel/alectryon
Author: Clément Pit-Claudel
Author-email: clement.pitclaudel@live.com
License: MIT
Location: /home/arthur/miniconda3/envs/exp/lib/python3.8/site-packages
Requires: pygments, beautifulsoup4, docutils, dominate
Required-by:
arthurpaulino commented 2 years ago

Ah, i just had to run eval $(opam env)