--copy-assets and -o

[jjhugues]

Hi,

TL;DR: --copy-assets copy copies assets in the input directory. I would have imagined it should copy them in an output directory if provided.

Imagine the following directory structure

./input
./input/d.v 
./output

I want to generate HTML pages in output using

alectryon  --no-header --frontend coqdoc --backend webpage  \
           input/d.v --copy-assets copy -o output/index.html

I get the following instead, forcing a manual move of assets to output

./input
./input/alectryon.css
./input/d.v
./input/alectryon.js
./output
./output/index.html

[cpitclaudel]

Do you have a recipe to reproduce the issue? I tried the following and I can't reproduce:

$ cd /tmp
$ mkdir bug-65
$ cd bug-65/
$ mkdir input output
$ echo "Check nat." > input/d.v
$ alectryon  --no-header --frontend coqdoc --backend webpage input/d.v --copy-assets copy -o output/index.html
$ tree
.
├── input
│   └── d.v
└── output
    ├── alectryon.css
    ├── alectryon.js
    ├── index.html
    └── pygments.css

[jjhugues]

Using your steps, plus some extra info on the installation. Could it be a portability issue on macOS?

➜  github git:(master) ✗ mkdir tmp
➜  github git:(master) ✗ cd tmp
➜  tmp git:(master) ✗ ls
➜  tmp git:(master) ✗ mkdir bug-65
➜  tmp git:(master) ✗ cd bug-65/
➜  bug-65 git:(master) ✗ mkdir input output
➜  bug-65 git:(master) ✗ echo "Check nat." > input/d.v
➜  bug-65 git:(master) ✗ alectryon  --no-header --frontend coqdoc --backend webpage input/d.v --copy-assets copy -o output/index.html
➜  bug-65 git:(master) ✗ tree
zsh: command not found: tree
➜  bug-65 git:(master) ✗ find .
.
./input
./input/alectryon.css
./input/d.v
./input/alectryon.js
./output
./output/index.html
➜  bug-65 git:(master) ✗ uname -a
Darwin mac-paleapple.fios-router.home 20.6.0 Darwin Kernel Version 20.6.0: Wed Jun 23 00:26:31 PDT 2021; root:xnu-7195.141.2~5/RELEASE_X86_64 x86_64
➜  bug-65 git:(master) ✗ alectryon --version
Alectryon v1.3.1
➜  bug-65 git:(master) ✗ python3 --version
Python 3.9.6
➜  bug-65 git:(master) ✗ opam list |grep coq
coq                     8.13.2        Formal proof management system
[..]
coq-serapi              8.13.0+0.13.0 Serialization library and protocol for machine interaction with the Coq proof assistant

[cpitclaudel]

Oh! Are you running the latest released version or from git master? If the former, then that explains it: I fixed the broken behavior that you're observing in 0bd97c01

[jjhugues]

I was about to report that forcing the output directory works:

bug-65 git:(master) ✗ alectryon --no-header --frontend coqdoc --backend webpage input/d.v --copy-assets copy -o output/index.html --output-dir=output

Yes, I use the latest released installed through opam. Good to know this is fixed, and that I have a work-around. Closing.