search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

can't include file in subdirectory with fslit #118

Closed msprotz closed 4 years ago

msprotz commented 4 years ago

I have a file in tutorial/spec/Spec.Bignum.fst and I'm trying to include it

.. toctree::
   Spec.Bignum
   Spec.Test
   Impl.Bignum.Lemmas
   Impl.Bignum
   Impl.Bignum.Intrinsics

but I get:

/Users/jonathan/Code/kremlin/book/Toy.rst:13: WARNING: toctree contains reference to nonexisting document 'Spec.Bignum'
/Users/jonathan/Code/kremlin/book/Toy.rst:13: WARNING: toctree contains reference to nonexisting document 'Spec.Test'
/Users/jonathan/Code/kremlin/book/Toy.rst:13: WARNING: toctree contains reference to nonexisting document 'Impl.Bignum.Lemmas'
/Users/jonathan/Code/kremlin/book/Toy.rst:13: WARNING: toctree contains reference to nonexisting document 'Impl.Bignum'
/Users/jonathan/Code/kremlin/book/Toy.rst:13: WARNING: toctree contains reference to nonexisting document 'Impl.Bignum.Intrinsics'
cpitclaudel commented 4 years ago

Can you give a self-contained example that I could reproduce the error with? (I haven't touched fslit in months ^^)

msprotz commented 4 years ago

yes -- both my issues are observable on branch protz_tutorial of kremlin

I'm available on the F* slack to help look at this... thanks for the fast responses! much appreciated

msprotz commented 4 years ago

The gist of the issue is that the .fst file I'm trying to include is in a subdirectory of a subdirectory of the root of the sphinx project -- somehow it doesn't seem to be resolved

msprotz commented 4 years ago

I'm closing this one because I figured out I had to just specify things like this:

.. toctree::
   tutorial/specs/Spec.Bignum
   tutorial/specs/Spec.Test
   tutorial/code/Impl.Bignum.Lemmas
   tutorial/code/Impl.Bignum
   tutorial/code/Impl.Bignum.Intrinsics

Thanks,

Jonathan