Missing _CoqConfig from InteractionTrees

[fairflow]

I have freshly installed coq and InteractionTrees after studying the ACM paper with our little Type Theory study group. I am new to this project and also it is very many years since I've used coq in earnest.

There are several issues with in running the tutorials and examples interactively using VSCode, though most of the make targets compile correctly (make all is ok, but with some warnings). Here is an interactive mode error in tutorial/Asm.v l28: From ITreeTutorial Require Import Fin Utils_tutorial.

Cannot find a physical path bound to logical path
Fin with prefix ITreeTutorial.

However, it does seem that a _CoqConfig is missing: evidence below. Whether adding references to that would help, I am not sure. Attempts to add a physical/logical connection have so far not succeeded (in fact I am unsure which file or files to edit to achieve this).

From header of generated _CoqProject file we have

# THIS IS AN AUTOMATICALLY GENERATED FILE
# PLEASE EDIT _CoqConfig INSTEAD

From Makefile we have the target:

depgraph:
	$(COQDEP) -dumpgraph $(DEPS_DOT) $(shell cat _CoqConfig) > /dev/null 2>&1
	sed 's%\("theories/\([^"]*\)/\([^"/]*\)"\[label="\)%\1\2/\\n%' -i $(DEPS_DOT)
	dot $(DEPS_DOT) -Tjpg -o$(DEPS_OUT)

Naturally, make depgraph fails.

My setup:

Apple silicon Mac 15.4.1 (24E263)
coq              8.20.1
coq-paco    4.2.3

[Lysxia]

Thanks for raising this issue. There is barely any documentation on how to build this project so it's normal to get stuck if you're not familiar with the build system. To address the problems you mentioned:

1. make all doesn't build the tutorial (maybe that should be fixed), that's probably why the interactive session fails. Try make tutorial.
2. _CoqConfig was renamed to _CoqProject.itree but I forgot to rename it also in the depgraph command. (The reasons why there's not simply a _CoqProject are that (1) I wanted to be able to add options to _CoqProject without having those changes seen by git, by putting those options in a local _CoqPath file, (2) now itree can also be built using dune, which requires a different _CoqProject to work with interactive editors, so the right _CoqProject depends even more on the user now.)