Oh, no, I see what was going on. The script of the student started with
import Pkg; Pkg.activate("ProjectName")
but when coding from VSCode, ProjectName was already active, such that that first line of the script created a subproject, and that messed up everything when it came to executing stuff.