Of course it is easy to workaround this by simply creating an Arend Run configuration with correct "Arend module" input:
However, it would be more intuitive if such Run Configuration was created and launched from the popup-menu for Arend directories (in the same fashion this currently works for .ard-files).
In Arend popup there is automatic launcher for type checking whole Arend file but there is no comparable launcher for directories. See video below:
https://github.com/JetBrains/intellij-arend/assets/7237597/1a929f52-03ce-4992-95fb-46e7f061aad6
Of course it is easy to workaround this by simply creating an Arend Run configuration with correct "Arend module" input:
However, it would be more intuitive if such Run Configuration was created and launched from the popup-menu for Arend directories (in the same fashion this currently works for .ard-files).