Failed to load file.
DUVELA opened this issue · 2 comments
DUVELA commented
sorry not Idris2.
Hi.
I was following the TDD idris book (10.3.3 TestStore.idr) in AMD fx8300 windows 10 visual studio code. However, I saw 'Failed to load file'. Is there any way? (In Atom and other extensions it works.)
meraymond2 commented
Hi, apologies for taking so long to get back to you.
It could be a number of things, I'd need a reproducible example to know for sure. If you're still facing this issue, can you check the extension settings, and make sure Idris2 Mode isn't on?
DUVELA commented
<!--
/* Font Definitions */
@font-face
{font-family:Gulim;
panose-1:2 11 6 0 0 1 1 1 1 1;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:"Malgun Gothic";
panose-1:2 11 5 3 2 0 0 2 0 4;}
@font-face
{font-family:GulimChe;
panose-1:2 11 6 9 0 1 1 1 1 1;}
@font-face
{font-family:"Malgun Gothic";}
@font-face
{font-family:Gulim;
panose-1:2 11 6 0 0 1 1 1 1 1;}
@font-face
{font-family:GulimChe;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
text-align:justify;
text-justify:inter-ideograph;
text-autospace:none;
word-break:break-hangul;
font-size:10.0pt;
font-family:"맑은 고딕",sans-serif;}
h1
{mso-style-priority:9;
mso-style-link:"\C81C\BAA9 1 Char";
margin:0cm;
text-align:justify;
text-justify:inter-ideograph;
page-break-after:avoid;
text-autospace:none;
word-break:break-hangul;
font-size:14.0pt;
font-family:"맑은 고딕",sans-serif;
font-weight:normal;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
code
{mso-style-priority:99;
font-family:GulimChe;}
span.1Char
{mso-style-name:"\C81C\BAA9 1 Char";
mso-style-priority:9;
mso-style-link:"\C81C\BAA9 1";
font-family:"맑은 고딕",sans-serif;}
.MsoChpDefault
{mso-style-type:export-only;}
/* Page Definitions */
@page WordSection1
{size:612.0pt 792.0pt;
margin:3.0cm 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
-->Hi, My English level is so bad. I’m forgot this issue. 😃 Idris1 only (not install Idris2)C:\Users\i>idris --version1.3.3 Vscode idris extenstionIdris Language v0.0.12 I solved it like this:One is to use atoms.Another is to add it to C:\idris\libs\libs\base\TDD .(like ‘import Data.Vect’ TDD was use mkdir. ) Windows용 메일에서 발송된 메일입니다. 보낸 사람: meraymond2보낸 날짜: 2022년 3월 30일 수요일 오후 5:10받는 사람: meraymond2/idris-vscode참조: -; Author제목: Re: [meraymond2/idris-vscode] Failed to load file. (Issue #78) Hi, apologies for taking so long to get back to you.It could be a number of things, I'd need a reproducible example to know for sure. If you're still facing this issue, can you check the extension settings, and make sure Idris2 Mode isn't on?—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you authored the thread.Message ID: ***@***.***>